Felix Cherubini

I think I solved the same issue for the RingSolver in the cubical library, which made the examples here work: [https://github.com/agda/cubical/blob/master/Cubical/Algebra/RingSolver/Examples.agda](https://github.com/agda/cubical/blob/master/Cubical/Algebra/RingSolver/Examples.agda) I had to sacrifice the generality of AlmostRings for...

Here is short recap of the problem (all rings commutative): What (my version of) the ring solver essentially does is to use equality of multivariate polynomials (over the integers) to...

Same origin, I looked at @oisdk 's solver and the paper it is based on. I didn't read everything though.

I don't think it is too much effort, if we do it together - I don't know much about the stdlib. Maybe that's a project for the agda implementer meeting?...

I'll start to look into that now.

There is a a problem I didn't think of yet. In the reflection code, in the function ```constructCallToSolver```, the given ring is substituted into a lambda. As far as I...

I think it is enough to just lift DB indices. I wrote something I am not proud of for the cubical library, which works in the cases I am interested...

That might be just what we need... I'll look into it and start PRs accordingly if it works/comment here if it doesn't.

I discussed this with @andreasabel and we concluded that the weakening function in the code you mentioned should do what we need. It might take a bit of time, until...

The situation is a bit more complicated than I thought: The code that constructs the call to the ring sovler is different than what I did in cubical library. Does...