@@ -284,6 +284,8 @@ data STrans : (m : Type -> Type) ->
284284 STrans m b (st2_fn result) st3_fn) ->
285285 STrans m b st1 st3_fn
286286 Lift : Monad m => m t -> STrans m t ctxt (const ctxt)
287+ RunAs : Applicative m => STrans m t in_res (const out_res) ->
288+ STrans m (m t) in_res (const out_res)
287289
288290 New : (val : state) ->
289291 STrans m Var ctxt (\lbl => (lbl ::: state) :: ctxt)
@@ -347,6 +349,7 @@ runST env (Bind prog next) k
347349runST env (Lift action) k
348350 = do res <- action
349351 k res env
352+runST env (RunAs prog) k = runST env prog (\res, env' => k (pure res) env')
350353runST env (New val) k = k MkVar (val :: env)
351354runST env (Delete lbl prf) k = k () (dropVal prf env)
352355runST env (DropSubCtxt prf) k = k (dropEnv env prf) (keepEnv env prf)
@@ -384,6 +387,11 @@ export
384387lift : Monad m => m t -> STrans m t ctxt (const ctxt)
385388lift = Lift
386389
390+export
391+runAs : Applicative m => STrans m t in_res (const out_res) ->
392+ STrans m (m t) in_res (const out_res)
393+runAs = RunAs
394+
387395export
388396new : (val : state) ->
389397 STrans m Var ctxt (\lbl => (lbl ::: State state) :: ctxt)