search

agda / cubical

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

NatSolver should be able to deal with 'suc's #1043

Closed felixwellen closed 11 months ago

felixwellen commented 11 months ago

This PR fixes an issue in the reflection interface of the NatSolver. Now any 'suc x' is translated correctly to '1 + x' in the Nat-Expression language which is used for solving. I also removed some unused code.

felixwellen commented 11 months ago

@mzeuner you might be interested in this fix... There is not much reviewing to be done here (as long as you don't ask to improve anything else in the solver, but I won't have time to do that anyway), but maybe you have a comment.

felixwellen commented 11 months ago

Since it is only a small bug fix, including a test, I'll just merge that.