comparison lib/ur/monad.urs @ 1172:ad15700272f6

Changing foldRX to mapX
author Adam Chlipala <adamc@hcoop.net>
date Sun, 28 Feb 2010 13:06:10 -0500
parents 8d3aa6c7cee0
children 79f487f51d9f
comparison
equal deleted inserted replaced
1171:7a2a7a8f9cab 1172:ad15700272f6
32 -> [[nm] ~ rest] => 32 -> [[nm] ~ rest] =>
33 tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest))) 33 tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
34 -> tr [] 34 -> tr []
35 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r) 35 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)
36 36
37 val mapR0 : K --> m ::: (Type -> Type) -> monad m
38 -> tr :: (K -> Type)
39 -> (nm :: Name -> t :: K -> m (tr t))
40 -> r ::: {K} -> folder r -> m ($(map tr r))
41
37 val mapR : K --> m ::: (Type -> Type) -> monad m 42 val mapR : K --> m ::: (Type -> Type) -> monad m
38 -> tf :: (K -> Type) 43 -> tf :: (K -> Type)
39 -> tr :: (K -> Type) 44 -> tr :: (K -> Type)
40 -> (nm :: Name -> t :: K -> tf t -> m (tr t)) 45 -> (nm :: Name -> t :: K -> tf t -> m (tr t))
41 -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tr r)) 46 -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tr r))