Jesper Cockx

Two more proposals by David Thrane Christiansen on Mastodon: - Disable eta-equality for records (if we don't remove them completely) - Enable `--exact-split`

> These look like linting rules to me. Could it be implemented as a standalone program using the Agda parser as a library? I suppose they could, though it would...

> Or rather: disable positional implicit arguments (only allow passing them by name). 😜 I see a lot of newcomers getting confused by the `{x = x}` syntax, so I'm...

> These look like linting rules to me. Could it be implemented as a standalone program using the Agda parser as a library? See also https://github.com/agda/agda/issues/7008

> Copatterns make Agda simpler! The notation should be extended! The assumption that we only ever do a bunch of left stuff then a bunch of right stuff has been...

> I think 'we' still haven't (pace the desire for a 'simple Agda') developed a good way to cash out the old-skool signature/structure distinction for dependently-typed APIs I agree that...

I approve!

It could be as a section under "getting started"?

After the fix of #4037 (https://github.com/agda/agda/commit/3d0dc0b2c3a7933a2e4986d9a073fbde385c2ecd) you now get an error message: ``` Cannot split because Issue3209a.A⁺.a is not in scope when checking that the expression ? has type A⁺...

That's true :/ I took a look at this issue but I have no idea how to fix it. If it remains unfixed for the release perhaps it's better to...