@@ -136,9 +136,7 @@ relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs
136136data Eff : (x : Type)
137137 -> (es : List EFFECT)
138138 -> (ce : x -> List EFFECT) -> Type where
139− value : a -> Eff a xs (\v => xs)
140− with_val : (val : a) -> Eff () xs (\v => xs' val) ->
141− Eff a xs xs'
139+ value : (val : a) -> Eff a (xs val) xs
142140 ebind : Eff a xs xs' ->
143141 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''
144142 callP : (prf : EffElem e a xs) ->
@@ -182,7 +180,7 @@ pure : a -> Eff a xs (\v => xs)
182180pure = value
183181
184182pureM : (val : a) -> Eff a (xs val) xs
185−pureM val = with_val val (pure ())
183+pureM = value
186184
187185(<$>) : Eff (a -> b) xs (\v => xs) ->
188186 Eff a xs (\v => xs) -> Eff b xs (\v => xs)
@@ -207,7 +205,6 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k
207205
208206eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b
209207eff env (value x) k = k x env
210−eff env (with_val x prog) k = eff env prog (\p', env' => k x env')
211208eff env (prog `ebind` c) k
212209 = eff env prog (\p', env' => eff env' (c p') k)
213210eff env (callP prf effP) k = execEff env prf effP k