Felix Cherubini

I think we should just not set it - the library fails with the current release candidate for agda 2.6.4.1 (with a heap-exhausted error) and checks if the option for...

Are you aware of the parallel PR: https://github.com/agda/cubical/pull/1093 where I try to improve the reflection code of the ringSolver a bit. Maybe there is a chance to share some code?...

I am still working towards a wild cat solver, starting with free wild cats here: #1117 Should we coordinate?

I made an issue which we can use to coordinate: #1118

Is it ready to merge?

With latest master, the code above _does not_ produce an internal error, but instead it is now something like: ``` /home/felix/agda/test/Fail/Issue5257.agda:7,1-17 Could not parse the left-hand side Bar (x ::...

I think this error message is reasonable enough -> closing.

It currently works on release-2.6.3 and I didn't figure out where it started to work (=give a reasonable error).

ping @MatthiasHu

This is now part of #1007 -> closing.