kdrag.parsers.microlean.define

kdrag.parsers.microlean.define(tree: Tree, env: Env) → FuncDeclRef

Parse a definition.

>>> tree = lark.Lark(grammar, start="define", parser="lalr").parse("def add1 (x : Int) : Int := x + 1")
>>> define(tree, Env(locals={}, globals={})).defn
|= ForAll(x, add1(x) == x + 1)

Parameters:

• tree (Tree)

• env (Env)

Return type:

FuncDeclRef