comparison lib/ur/monad.urs @ 1310:f0909fb3848f

Simplify type of Monad.appR2
author Adam Chlipala <adam@chlipala.net>
date Sun, 17 Oct 2010 13:26:11 -0400
parents fd1a49b51db5
children 726f0caeea3f
comparison
equal deleted inserted replaced
1309:127561e4aef1 1310:f0909fb3848f
61 -> tr [] 61 -> tr []
62 -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tf' r) * tr r) 62 -> r ::: {K} -> folder r -> $(map tf r) -> m ($(map tf' r) * tr r)
63 63
64 val appR2 : K --> m ::: (Type -> Type) -> monad m 64 val appR2 : K --> m ::: (Type -> Type) -> monad m
65 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) 65 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
66 -> (nm :: Name -> t :: K -> rest :: {K} 66 -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m unit)
67 -> [[nm] ~ rest] =>
68 tf1 t -> tf2 t -> m unit)
69 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m unit 67 -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m unit