Jon Sterling
Jon Sterling
Can we think of a better notation? It's so ugly. Honestly, comp is bad too when it is dependent.
Noticed this with @kaonn today; I'll try and troubleshoot & fix
Right now, the only kind of "argument type" allowed is just `Self`; this should be generalized to `A -> Self`, where `A` is a type. Combining this with #200, the...
The “generalize” tactic is useful. We should expose it to the user!
So much duplication! So much opportunity for bugs!
When using generalization tactics, it's helpful to be able to hide the dummy hypotheses that were generalized away. Really there seems to be no actual reason to delete them; we...
This is something that was first noticed by favonia a while back, but I wanted to write it down so that we can theorize a fix. A diagonal dimension action...
As far as I understand, Agda's (idealized) core type theory has only top-level definitions, rather than allowing an eliminator to be applied at any point in the program. This doesn't...