kdrag.printers.latex.to_latex_goal

kdrag.printers.latex.to_latex_goal(goal: Goal) → str

>>> x = smt.Int("x")
>>> g = tactics.Goal(sig=[x], ctx=[x > 0, x < 10], goal=x == 5)
>>> to_latex_goal(g)
'\\begin{array}{ll} \\text{fix} & \\text{x} : \\mathsf{Int} \\\\ h_{0} & \\text{x} > 0 \\\\ h_{1} & \\text{x} < 10 \\\\ \\hline \\vdash & \\text{x} = 5 \\end{array}'
>>> to_latex_goal(tactics.Goal.empty())
'\\text{Nothing to do!}'

Parameters:

goal (Goal)

Return type:

str