Implements equational definitions as described in #34. When h.def is present in the context for a symbol h that we should define (a hint h in smt [h]), we default to the eqn def rather than using Lean's own unfolding theorem. There are no uses of this mechanism in this PR, but I have some here.
Implements equational definitions as described in #34. When
h.defis present in the context for a symbolhthat we should define (a hinthinsmt [h]), we default to the eqn def rather than using Lean's own unfolding theorem. There are no uses of this mechanism in this PR, but I have some here.