o2v1
Convert a primo certificate into a coq proof
Usage
o2v [-split]
[-n
theorem]
[-o
filename]
primocertif
Overview
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
Releases
Unchanged in 2 releases since Debian 12 (Bookworm).