Mercurial > urweb

comparison lib/ur/monad.urs @ 2185:cbd294994c69

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Monad.mapR3
author Adam Chlipala <adam@chlipala.net>
date Sat, 31 Oct 2015 11:49:30 -0400
parents a613cae954ca
children
comparison
equal deleted inserted replaced
2184:1ecef02f67c5 2185:cbd294994c69
56 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) 56 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
57 -> tr :: (K -> Type) 57 -> tr :: (K -> Type)
58 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t)) 58 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m (tr t))
59 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r)) 59 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m ($(map tr r))
60 60
61 val mapR3 : K --> m ::: (Type -> Type) -> monad m
62 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type)
63 -> tr :: (K -> Type)
64 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> tf3 t -> m (tr t))
65 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m ($(map tr r))
66
61 val foldMapR : K --> m ::: (Type -> Type) -> monad m 67 val foldMapR : K --> m ::: (Type -> Type) -> monad m
62 -> tf :: (K -> Type) 68 -> tf :: (K -> Type)
63 -> tf' :: (K -> Type) 69 -> tf' :: (K -> Type)
64 -> tr :: ({K} -> Type) 70 -> tr :: ({K} -> Type)
65 -> (nm :: Name -> t :: K -> rest :: {K} 71 -> (nm :: Name -> t :: K -> rest :: {K}