Print Theorems as Latex (without proof)

[jngross95]

Dear LeanTex developers,

I would like to automatically convert Lean theorems (without proof) into LaTeX code. However, I am unsure how to use the library. The project provides examples of how to test the library, where the LaTeX code needs to be entered. How can I convert terms in my own project? How can I write a method like #print_latex my_theorem?

Example:

theorem my_theorem{R : Type*} [Field R]  (a b c d: R) (hb : b ≠ 0) (hd : d ≠ 0)  :

      (a / b) * (c / d) = (a*c) / (b*d) := by

field_simp [hb, hd]

#print_latex my_theorem

output:

$\frac{a}{b} \cdot \frac{c}{d} = \frac{a \cdot c}{b \cdot d} $

Possibly also with the hypotheses $b \neq 0, d \neq 0$ and the types $a b c d : R$.

Latex-Code:

\frac{a}{b} \cdot \frac{c}{d} = \frac{a \cdot c}{b \cdot d}  

[kmill]

The library is meant to be used in other programs rather than be used directly, and the commands provided are for testing purposes. If you have some metaprogramming knowledge, you could adapt the commands for your purposes.

However, if you want to output the latex for some specific theorem, you could do something like this:

#latex type_of% @my_theorem
/-
\forall R : \mathbf{Type},\ \forall inst : \text{Field}_{R},
\ \forall a : R,\ \forall b : R,\ \forall c : R,\ \forall d : R,\ b \neq 0 \implies
\left(d \neq 0 \implies \frac{a}{b} \cdot \frac{c}{d} = \frac{a \cdot c}{b \cdot d}\right)
-/

(Note that https://github.com/kmill/LeanTeX-mathlib now exists too, which is a place where mathlib-specific LaTeX pretty printers can go.)