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