kdrag.parsers.microlean.define

kdrag.parsers.microlean.define(s: str, globals=None) → FuncDeclRef

Parse a definition.

>>> define("def add1 (x : Int) : Int := x + 1").defn
|= ForAll(x, add1(x) == x + 1)