Lennart Augustsson wrote: > Agda has made the choice that you can have (almost) any sequence of > characters in identifiers. It works fine, but forces you to use white > space (which I do anyway). No _'s though, which is exactly what Jason was after. :-) Still, Agda rocks. Martijn.