Andreas Abel

Mmh, I have to investigate whether the (newish) _termination_ check for record types is more precise than the _guardedness_ (positivity) check. Then the language change could be smaller.

Since I am fixing #4343, I can maybe document the status quo. > If you import a module you also get all of its rewrite rules, You also get the...

> Since I am fixing [#4343](https://github.com/agda/agda/issues/4343), in #7934, maybe you can have a look @jespercockx .

It seems that the current semantics of ```agda f ps = rhs module M where defs ``` is, assuming `Delta` is the telescope of the pattern variables of patterns `ps`,...

@jespercockx : Can you test this PR on your REWRITE examples, also the confluence examples and check whether introduces any regressions? I think we are lacking a complicated module structure...

> @andreasabel asked me if I had any project that uses rewrite rules. Here is one: https://github.com/ecavallo/equivariant-cartesian Thanks, seems that my PR breaks this. On a fresh checkout, I get...

I replaced the PR by a new fix and now it passes @ecavallo 's development. Yay!

Added documentation for importing rewrite rules (closing #7935).

@jespercockx : I am planning to merge this today and make a new RC; this is currently the last open release-blocker. So if you want to evaluate it further, please...

This can be shrunk to just: ```agda open import Agda.Primitive variable l : Level record R (A : Set l) : Set where test : {A : Set l} (r...