agda/cubical

Make the CommRingSolver work better with concrete rings

Opened this issue · 0 comments

As pointed out in the examples for the CommRingSolver, there are problems with using concrete rings, e.g. the integers.
This is due to the normalisation of the goal that currently happens before the actual parsing of the ring expressions. To fix the problem, it might be enough to just not normalise the goal and introduce matching for the binary minus ´´´_-_´´´.