Man page - o2v(1)
Packages contas this manual
Package: coqprime-tools
apt-get install coqprime-tools
apt-get install coqprime-tools
Manuals in package:
Documentations in package:
Manual
| O2V(1) | General Commands Manual | O2V(1) |
NAME
o2v - convert a primo certificate into a Coq proof
SYNOPSIS
o2v [-split] [-n theorem] [-o filename] primocertif
DESCRIPTION
This tool takes a certificate file generated by primo (https://ellipsa.eu) and turns it into a Coq proof script.
OPTIONS
-split Generate one proof by certificate in the primo file
- -n <theorem>
- Name of the final theorem in the Coq proof
- -o <filename>
- Prints the proof script in the file named <filename> (otherwise: FirstPrimes.v)
- <primocertif>
- Name of the primo certification file
| July 15th, 2022 |