kdrag.printers.lean.decl_axiom

kdrag.printers.lean.decl_axiom(f: FuncDeclRef) → str

Convert a function declaration to a Lean axiom definition.

>>> f = smt.Function("f", smt.IntSort(), smt.IntSort(), smt.BoolSort())
>>> decl_axiom(f)
'axiom f : Int -> Int -> Bool\n'