ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 14:57:30 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #1364 from puffnfresh/neweffects-bad-constraints

Browse Source 
Remove bad Applicative constraints from neweffects
This commit is contained in:
Edwin Brady 2014-07-08 12:29:36 +01:00
commit 99ebe20f15
1 changed files with 5 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
libs/neweffects/Effects.idr
View File

@ -272,20 +272,19 @@ runEnv env prog = eff env prog (\r, env => pure (r ** env))
-- ----------------------------------------------- [ some higher order things ]
mapE : Applicative m => (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)
mapE : (a -> {xs} Eff b) -> List a -> {xs} Eff (List b)
mapE f [] = pure []
mapE f (x :: xs) = [| f x :: mapE f xs |]
mapVE : Applicative m =>
(a -> {xs} Eff b) ->
Vect n a ->
{xs} Eff (Vect n b)
mapVE : (a -> {xs} Eff b) ->
Vect n a ->
{xs} Eff (Vect n b)
mapVE f [] = pure []
mapVE f (x :: xs) = [| f x :: mapVE f xs |]
when : Applicative m => Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()
when True e = Force e
when False e = pure ()