logo
Free, unlimited AI code reviews that run on commit
git-lrc git-lrc GitHub Install Now We'd appreciate a star git-lrc - Free, unlimited AI code reviews that run on commit | Product Hunt git-lrc - Free, unlimited AI code reviews that run on commit | Product Hunt

o2v - convert a primo certificate into a Coq proof

Description

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

Name

       o2v - convert a primo certificate into a Coq proof

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                                          O2V(1)

Synopsis

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

See Also