kdrag.parsers.microlean.lean

kdrag.parsers.microlean.lean(s: str, globals=None) → ExprRef

Alias for parse to match Lean users’ expectations.

>>> foo = smt.Int("foo1")
>>> lean("foo + 2")
foo1 + 2

Parameters:

s (str)

Return type:

ExprRef