agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
441 stars 134 forks source link

Refactor and improve CommRingSolver #1093

Closed felixwellen closed 5 months ago

felixwellen commented 5 months ago

The reflection code of the CommRingSolver is pretty horrible, this PRs intends to improve the situation and make it more flexible.

felixwellen commented 5 months ago

Now it should be more easy to guess when the ring solver will work: It doesn't work well with concrete rings like the integers and sometimes you need to introduce helpers, if some meta variables cannot be solved. Otherwise it should work now in place as one might expect.

felixwellen commented 5 months ago

Max agreed to a merge -> merging.