Edwin Brady ff619951f0 Reorganise LIO to allow 'pure' ... Doing this is awkward, for a number of reasons, including 'pure' not being linear in its argument - there's no guarantee it'll be used linearly after all - and lack of multiplicity polymorphism. Fortunately the user doesn't have to know about the ugliness underneath! We can look at ways to make it less horrible later :). For now, this is starting to look like something that allows us to write linear protocols without too much extra machinery on top of IO.		2020-06-24 21:24:15 +01:00
..
LIO.idr	Reorganise LIO to allow 'pure'	2020-06-24 21:24:15 +01:00