[alexanderdmitri]

once you've started on Idris you've crossed the line over from kinky to deviancy

source: there are several people in my weekly support group for exactly this reason, it gets out of control

[Blikkentrekker]

I would trust any type system that doesn't require me to prove that my sorting algorithm maintains the length of the vector it sorts.