@@ -593,15 +593,13 @@ runLoop fuel prog onEmpty
593||| responsibility of an implementation of an interface in IO which uses it
593||| responsibility of an implementation of an interface in IO which uses it
594||| to ensure that it isn't duplicated.
594||| to ensure that it isn't duplicated.
596−runWith : {resf : _} ->
597− Env res -> STrans IO a res (\result => resf result) ->
596+runWith : Env res -> STrans IO a res resf ->
598 IO (result ** Env (resf result))
597 IO (result ** Env (resf result))
599runWith env prog = runST env prog (\res, env' => pure (res ** env'))
598runWith env prog = runST env prog (\res, env' => pure (res ** env'))
602−runWithLoop : {resf : _} ->
603− Env res -> Fuel -> STransLoop IO a res (\result => resf result) ->
601+runWithLoop : Env res -> Fuel -> STransLoop IO a res resf ->
604− IO (Maybe (result ** Env (resf result)))
602+ IO (Maybe (result ** Env (resf result)))
605runWithLoop env fuel prog
603runWithLoop env fuel prog
606 = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))
604 = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))
607 (pure Nothing)
605 (pure Nothing)