André Videla
André Videla
> manipulating FCs (for better error reporting, showing the correct type on hover, etc.) Do you have examples of this that we can study? I'm going to update the motivation...
Given the absolute nightmare that it was to simply keep the elab tree up to date with TTImp I think the best way to move forward is as follows: -...
Is this a feature of records or is this a feature of modules? I assumed it was the latter. edit: After some thinking I've come to the conclusion that we...
This came to bit me but I think the mechanism is a bit different. I get the same without relying on `type` but merely having a ω scrutinee: ```Idris import...
``` data D : Type where Abs : (D = e) -> (e -> Void) -> D lam : (D -> Void) -> D lam f = Abs Refl f...
what's the result of case-splitting?
All of this sounds good. Something I've been trying to unsuccessfully encourage in the past is to have PRs explain exactly what they are, why they exist, why they fix...
Something I would like to submit here as a new concept in the current process is the notion of an "accepted" issue/proposal vs one that is "in discussion" or "rejected"....
I just noticed this and how it's similar to something I'm already working on, quick question: Why do you want to use the `interface` mechanism rather than using records? Is...
For point number 1, what you're looking for is _copattern syntax_ https://agda.readthedocs.io/en/latest/language/copatterns.html I'm not quite sure I'm entirely sold on the design of the feature but if you can make...