kmill / leantex Goto Github PK

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}