Stefan Höck

> I am fairly certain this is due to #2954. Prior to PR #2953, the termination checker was accepting some functions for the wrong reason, masking issue #2954. > >...

For your info, there is an external library not maintained by the Idris core team which tries to provide such verified "interfaces". Maybe this could be useful for you as...

I once again invite you to have a look at idris2-algebra (if you haven't already done so). Personally, I think we should not write laws about interfaces but about sets...

> Actually `Ord` would be appropriate, as a commutative `+` is certainly enough to prove that `for all a, b, a < b exists c > 0, a = b...

> So trying to prove that (Int64, +, *) is a ring does not fail because you are bad at proving, but because that’s impossible because Int64 only has a...

> But if you define the ring as being the ring modulo n, it is impossible to define a (total) ordering that is compatible with the addition of the ring....

Thanks a lot for your suggestions @mattpolzin . Just a small note from my side: Every time we drop stuff from contrib we potentially break a lot of packages. I...

> @stefan-hoeck yeah, you're right that these changes are very likely to break packages. Do you suggest that something new be slotted into the process or are you aiming for...

Actually, I don't think this is a bug of the chez backend: The problem is already there when the `CExp` IR is being generated. The branch should be chosen from...

Could someone please update me on the status of this issue. Is this even something we can handle with pack?