Add support for `exists` quantifier.

ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.

Apache License 2.0

89 stars 18 forks source link

Closed abdoo8080 closed 2 years ago

abdoo8080 commented 2 years ago

This PR adds Exists constructor to the Term data-structure (similar to Forall). It also adds support for conversion from Nat to Int.