This PR adds support for defining constants in the Lean goal. Currently, those are treated as uninterpreted functions. This PR also fixes a bug where an assertion is not added for (first-order) functions that return a Nat (the returned value must not be less than zero).
This PR adds support for defining constants in the Lean goal. Currently, those are treated as uninterpreted functions. This PR also fixes a bug where an assertion is not added for (first-order) functions that return a
Nat(the returned value must not be less than zero).