@@ -407,13 +407,20 @@ runSTLoop (More x) env (Pure result) k onDry = k result env
408pure : (result : ty) -> STrans m ty (out_fn result) out_fn
408pure : (result : ty) -> STrans m ty (out_fn result) out_fn
409pure = Pure
409pure = Pure
412(>>=) : STrans m a st1 st2_fn ->
412(>>=) : STrans m a st1 st2_fn ->
413 ((result : a) -> STrans m b (st2_fn result) st3_fn) ->
413 ((result : a) -> STrans m b (st2_fn result) st3_fn) ->
414 STrans m b st1 st3_fn
414 STrans m b st1 st3_fn
415(>>=) = Bind
415(>>=) = Bind
418+returning : (result : ty) -> STrans m () ctxt (const (out_fn result)) ->
419+ STrans m ty ctxt out_fn
420+returning res prog = do prog
418lift : Monad m => m t -> STrans m t ctxt (const ctxt)
425lift : Monad m => m t -> STrans m t ctxt (const ctxt)
419lift = Lift
426lift = Lift