kdrag.parsers.microlean.theorem

kdrag.parsers.microlean.theorem(tree: Tree, env: Env) → Proof

Parse a theorem.

>>> tree = lark.Lark(grammar, start="theorem", parser="lalr").parse("theorem add1_nonneg : forall x : Int, x >= x - 1 := grind")
>>> theorem(tree, Env(locals={}, globals={}))
|= ForAll(x, x >= x - 1)

Parameters:

• tree (Tree)

• env (Env)

Return type:

Proof