ufmg-smite / lean-smt

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

Sexp #14

Closed Vtec234 closed 2 years ago

Vtec234 commented 2 years ago

Depends on #13. I did not move the string-based commands over to the Sexp type (yet?) as this does not make emitting commands that much nicer, but I think it will be quite useful for parsing solver outputs to have them as Sexp rather than as String.