kdrag.printers.lean.of_expr

kdrag.printers.lean.of_expr(e: ExprRef)

>>> x,y,z = smt.Ints("x y z")
>>> of_expr(x)
'(x : Int)'
>>> of_expr(x + y + z)
'(((x : Int) + (y : Int)) + (z : Int))'
>>> of_expr(smt.If(x == x, y, z))
'(if ((x : Int) = (x : Int)) then (y : Int) else (z : Int))'

Parameters:

e (ExprRef)