ufmg-smite / lean-smt

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

Unfold type class projections. #21

Closed abdoo8080 closed 2 years ago

abdoo8080 commented 2 years ago

This PR unfolds all type class projections before processing expressions, removing a lot of type class arguments in the process. This change allows us to remove the two biggest hacks in the codebase: the transformers that indiscriminately remove type arguments and type class instance arguments. There are some corner cases where those arguments are not removed by unfolding the projections. Those are now handled in a case-by-case manner.