search

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.
Apache License 2.0
94 stars 19 forks source link

Let-binding terms #28

Closed Vtec234 closed 2 years ago

Vtec234 commented 2 years ago

Just adds basic support for emitting let bindings. I will add the local let to define-fun translation in another PR.

Vtec234 commented 2 years ago

(Sorry about the slightly unreadable diff. You can select 'Hide whitespace' in the GitHub diff view to hide indent changes.)

Vtec234 commented 2 years ago

Rebased on the recursion branch and undid the local-let to define-fun translation, I will do it differently.