search

ufmg-smite / lean-smt

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

Add `TransformerM` monad to simplify `mark*` functions. #4

Closed abdoo8080 closed 2 years ago

tomaz1502 commented 2 years ago

This is way more clean, indeed! The only thing that is bothering me a little bit is that we're ignoring the output of the State monad. Do you know if there is any alternative monad that acts just like the State but doesn't have the output?

tomaz1502 commented 2 years ago

Hmm, maybe this doesn't make sense, since the bind operator won't have a type to work on... well, I will approve the changes, but let me know if you know some way to make this work