-- https://github.com/idris-lang/Idris-dev/blob/master/samples/ST/Intro.idr undefined as rforall a. a undefined = 0 assert :: {v:Bool | v} -> Unit assert = \tru -> Unit ----------------------------------------------------------------------------- -- | Library ---------------------------------------------------------------- ----------------------------------------------------------------------------- bind :: rforall a, b, p, q, r. ST
q >a ->
(x:a -> ST r >b
bind = undefined
thenn :: rforall a, b, p, q, r.
ST r >b) ->
ST