Mercurial > urweb
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)) |