G. Allais
G. Allais
I suspect the issue is that we see `{0 a : Type}` and assume for coverage checking purposes that `a = Nat` is a forced pattern rather than a type...
I should perhaps just give up on this stuff
Turn them into internal-error feedback!
Thinking about getting a text editor based on https://codemirror.net/try/ and syntax highlighting based on https://lezer.codemirror.net/ for syrup
This would allow us to get the emacs mode to point to the location of errors
To stop student from computing the truth table for a 8 inputs circuit
Snoclists (lists that grow on the right rather than the left) are commonly used when representing syntaxes with binding because they grow the same way contexts grow which allows you...