> I got confused by the infix definition of "~>*". Aaah, I'm sorry -- I thought you meant the theorem body -- the proof itself -- was hard to parse. (Which it

> I got confused by the infix definition of "~>*". Aaah, I'm sorry -- I thought you meant the theorem body -- the proof itself -- was hard to parse. (Which it also is!) Yes, custom infix operators are just one of many novelties you can find in these languages. I think Haskell is the only "mainstream" (hah) language I'm familiar with that has anywhere close to the same degree of syntax customization. All these things together really do make for a steep learning curve...