Generating latex from coq theorems (Coq to Latex)

Using Coq
1

I wanted to generate latex from coq. Not sure what the different options that exist but one that would be nice for me would be to do it in coqtop (or serapi) e.g.

print_coq2latex theorem_name.

or

print_coq2latex forall n: Nat, n + 0 = n.
$ forall n \in \matbbb N, n + 0 = n $ (or whatever latex)

Generating latex files might be fine too but the focs here don’t provide concrete examples of how to actually do this coq to latex feature.

How does one do this?

2

Among other options, you may use Alectryon, which allows you to control which parts of code, sub-goals, and answers you want to print, and in which order you will display them in the final document.

In this paper we describe how we use Alectryon to generate a 300p document, in which all the inclusions of Coq code are consistent with the described library.

Btw, which information is missing from coqdoc’s doc ?

3 Likes