Jesper Cockx

In that case I do not have a problem with this addition, though I do not really see the point of it personally.

I'm considering to give this a try, but change a bit how rewrite rules on projections would work. In particular, I propose that we should be able to declare rewrite...

I'm trying again to make this work and I've been able to make some progress on the internal errors that were occurring in my previous attempt. However, now I'm stuck...

I'd still very much like to implement this, but I currently have other priorities. My WIP can be found on https://github.com/jespercockx/agda/tree/rewriting-projections, if anyone wants pointers on where I got stuck...

I've rebased my branch at https://github.com/jespercockx/agda/tree/rewriting-projections onto a recent version of Agda and tried to run the tests. Basic tests with rewriting projections work, but there are a lot of...

But I like this feature :(

Seems that this is blocking #5810, so I'm moving it to the 2.6.3 milestone. Would you be ok with simply changing the levels so they do not depend on `I`?

I'd be interested in taking a look at the unification problem on which the LHS unifier is slow. Currently it is still very unoptimized, but since I never had an...

How do other programming languages handle this (e.g. Haskell, Coq, Idris, ...)? This does not seem like a problem where we should try to reinvent the wheel.

Here is a minimal reproducer: ```agda {-# OPTIONS --rewriting #-} open import Agda.Builtin.Unit open import Agda.Builtin.Equality open import Agda.Builtin.Equality.Rewrite X : Set postulate ν : Set → Set → X...