G. Allais

Pattern synonyms don't lead to cleaner goals which is the point of this.

I just had my last lecture for this (academic) year earlier today so should have a bit of time reasonably soon-ish to take this on :)

I think we absolutely need to break the symmetry for the cons/snoc. I am happy to revert the cosmetic distinction between `[]`. As for the cons-right symbol, I'm afraid it's...

@joelberkeley You can use induction-recursion to define a dictionary together with a notion of key freshness and insist that all new keys must be fresh. ```idris import Data.So record Distinct...

> refactor a number of existing records into either `Record` or `WithData`. Built-in records have constant time access to their fields but for `Record` it's linear in the index. Isn't...

> Can anyone come up with a method that can handle most or all of the cases I've listed? Thinking out loud: could'nt we have a small language of directives...

`∃ (\x → x ∈ xs × P x))` is essentially `Any P xs` as [`find`](https://agda.github.io/agda-stdlib/Data.List.Membership.Setoid.html#1435) demonstrates. So you can get that by using [`any`](https://agda.github.io/agda-stdlib/Data.List.Relation.Unary.Any.html#2832), then cast `Dec` to a...

In "Generic Level Polymorphic N-ary Functions", I have ```agda decide : Π[ P ∪ Q ] → Π[ Any P ∪ All Q ] ``` It seems to also be...

I don't think so. You could use [`Any`'s `_─_`](https://agda.github.io/agda-stdlib/Data.List.Relation.Unary.Any.html#2197) together with [`Any`'s `any`](https://agda.github.io/agda-stdlib/Data.List.Relation.Unary.Any.html#2832).

I'm happy to go ahead with this.