> ... And notice how the syntax in that message isn't even close to valid Agda!
That is unfair: I copied the type annotations from random places in the
Agda library (and then edited them to make them more interesting).
Stefan
PS: Of course, any sequence of chars (especially funny Unicode symbols)
is potentially valid Agda code (as long as you provide the appropriate
context).
