on master help sign in
Remove bad Applicative constraints from neweffects
commit8279c8059abb870230fed7d4d873d5595ad9a9f4 authorBrian McKenna <brian@brianmckenna.org> dateSun 6 Jul 2014, 16:46 (12 years ago) parent3c4bd14
1 file changed+5−6
libs/neweffects/Effects.idr+5−6
libs/neweffects/Effects.idr+5−6
@@ -272,20 +272,19 @@ runEnv env prog = eff env prog (\r, env => pure (r ** env))
272272
273273-- ----------------------------------------------- [ some higher order things ]
274274
275−mapE : Applicative m => (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)
275+mapE : (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)
276276mapE f [] = pure []
277277mapE f (x :: xs) = [| f x :: mapE f xs |]
278278
279279
280−mapVE : Applicative m =>
281− (a -> {xs} Eff b) ->
282− Vect n a ->
283− {xs} Eff (Vect n b)
280+mapVE : (a -> {xs} Eff b) ->
281+ Vect n a ->
282+ {xs} Eff (Vect n b)
284283mapVE f [] = pure []
285284mapVE f (x :: xs) = [| f x :: mapVE f xs |]
286285
287286
288−when : Applicative m => Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
287+when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
289288when True e = Force e
290289when False e = pure ()
291290