On: 'Rent-a-person who does nothing' in Tokyo receives...

[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 → alexanderdmitri]

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.