kdrag.parsers.microlean.axiom

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

Parse an axiom.

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

Parameters:

• tree (Tree)

• env (Env)

Return type:

Proof