Man page - o2v(1)

Packages contains this manual

Package: coqprime-tools
apt-get install coqprime-tools

Manuals in package:

Documentations in package:

o2v - convert a primo certificate into a Coq proof

o2v [-split] [-n theorem] [-o filename] primocertif

This tool takes a certificate file generated by primo (https://ellipsa.eu) and turns it into a Coq proof script.

-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