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