kdrag.printers.latex.to_latex

kdrag.printers.latex.to_latex(obj: ExprRef | SortRef | Proof | Goal | ProofState, prec: int = 0) → str
>>> x = smt.Int("x")
>>> to_latex(x + 1)
'\\text{x} + 1'
>>> to_latex(smt.IntSort())
'\\mathsf{Int}'
>>> to_latex(kd.prove(x < x + 1))
'\\vdash \\text{x} < \\text{x} + 1'
>>> l = tactics.Lemma(x > 0)
>>> to_latex(l)
'\\begin{array}{ll} \\hline \\vdash & \\text{x} > 0 \\end{array}'
Parameters:
Return type:

str