Jacques Carette
Jacques Carette
Indeed - those should be hard errors.
I would say either "defined types" or "enumerated types". In either case, it involves user-defined types. Quasi-types sounds too mystical... > We define Z^+ as "any value of Z greater...
Doing this in small steps makes sense. Starting with `Object.Reasoning.Iso` seems like a good idea. Regarding the 3 steps of your proposed solution, I would think that doing them exactly...
What a wonderful discussion! My first instinct was to reply along the same lines as what @MatthewDaggitt said, as my experience of wiring in specific proofs lead to `subst`-hell too....
On the 'not that simple', it starts with a simple observation: let G and H be enormous numbers (like Graham's number or TreeT(4), which are expressible in Agda but effectively...
Note that your two examples could be handled without explicit DISPLAY rules (which would be a 'big' feature, potentially prone to bugs): if those two definitions could be marked as...
Surprised that no one's commented yet: yes, this does seem like a rather handy feature. I've certainly seen a lot of noise on social media from people who think that...
These proposed extensions sure make a lot sense to me.
You should make shorter titles and longer descriptions. And in descriptions, you can use github's code linking features to show use exactly what the problem is and what the solution...
Good find @jackwyand We should first analyze what's going on with the pattern. Is it all meta-information? If so, then clearly we should abstract it out. In a way, that...