Add a `runEnv` document comment
commit1381cdb7edcc585a3b4ef536469b00bab34d94f1
authoraiya000 <aiya000.develop@gmail.com>
dateSun 18 Feb 2018, 21:30 (9 years ago)
parent6d7fd7b
libs/effects/Effects.idr+1
@@ -434,6 +434,7 @@ runPureInit env prog = eff env prog (\r, env => r)
434434runWith : (a -> m a) -> Env m xs -> EffM m a xs xs' -> m a
435435runWith inj env prog = eff env prog (\r, env => inj r)
436436
437+||| Similar to 'runInit', but take the result of `Env`.
437438%no_implicit
438439runEnv : Applicative m => Env m xs -> EffM m a xs xs' ->
439440 m (x : a ** Env m (xs' x))