ufmg-smite / lean-smt

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

Add more `QF_BV` builtins #43

Closed Vtec234 closed 1 year ago

Vtec234 commented 1 year ago

Adds most of the symbols except for some derived ones which we can translate into the definition directly, and for signed operations since the semantics of the default Fin arithmetic in Lean is unsigned (we could add them later if needed). Closes #41.