search

ufmg-smite / lean-smt

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

Add support for intro and ih. #5

Closed abdoo8080 closed 2 years ago

abdoo8080 commented 2 years ago

This PR adds support for context changes introduced by other tactics (e.g., intro and induction). It also changes the signature of Nat.sub to use Nat instead of Int.