Mercurial > urweb
comparison lib/ur/monad.urs @ 1313:0bf73c3e4563
Monad.appR3
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Tue, 19 Oct 2010 15:26:12 -0400 |
parents | 726f0caeea3f |
children | a613cae954ca |
comparison
equal
deleted
inserted
replaced
1312:726f0caeea3f | 1313:0bf73c3e4563 |
---|---|
68 | 68 |
69 val appR2 : K --> m ::: (Type -> Type) -> monad m | 69 val appR2 : K --> m ::: (Type -> Type) -> monad m |
70 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) | 70 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) |
71 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m unit) | 71 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m unit) |
72 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m unit | 72 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m unit |
73 | |
74 val appR3 : K --> m ::: (Type -> Type) -> monad m | |
75 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) | |
76 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> tf3 t -> m unit) | |
77 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m unit |