Add 'returning' to Control.ST
It is mostly there to help with interactive development - you can see
what the states should be before returning the value by writing
'returning val ?help' and checking the type of ?help
commitb5ea205c7649a06d6ce189d21cbe1346709b1b5e
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 20 Mar 2017, 17:14 (10 years ago)
parent698705e
libs/contrib/Control/ST.idr+8−1
@@ -407,13 +407,20 @@ runSTLoop (More x) env (Pure result) k onDry = k result env
407407export
408408pure : (result : ty) -> STrans m ty (out_fn result) out_fn
409409pure = Pure
410−
410+
411411export
412412(>>=) : STrans m a st1 st2_fn ->
413413 ((result : a) -> STrans m b (st2_fn result) st3_fn) ->
414414 STrans m b st1 st3_fn
415415(>>=) = Bind
416416
417+export
418+returning : (result : ty) -> STrans m () ctxt (const (out_fn result)) ->
419+ STrans m ty ctxt out_fn
420+returning res prog = do prog
421+ pure res
422+
423+
417424export
418425lift : Monad m => m t -> STrans m t ctxt (const ctxt)
419426lift = Lift