Mercurial > urweb
changeset 1310:f0909fb3848f
Simplify type of Monad.appR2
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 17 Oct 2010 13:26:11 -0400 |
| parents | 127561e4aef1 |
| children | 5337adf33a4a |
| files | lib/ur/monad.ur lib/ur/monad.urs |
| diffstat | 2 files changed, 3 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/monad.ur Thu Oct 14 11:54:54 2010 -0400 +++ b/lib/ur/monad.ur Sun Oct 17 13:26:11 2010 -0400 @@ -94,13 +94,11 @@ fl fun appR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] - (f : nm :: Name -> t :: K -> rest :: {K} - -> [[nm] ~ rest] => - tf1 t -> tf2 t -> m unit) + (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> m unit) [r ::: {K}] (fl : folder r) = @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m unit] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 => acc (r1 -- nm) (r2 -- nm); - f [nm] [t] [rest] ! r1.nm r2.nm) + f [nm] [t] r1.nm r2.nm) (fn _ _ => return ()) fl
--- a/lib/ur/monad.urs Thu Oct 14 11:54:54 2010 -0400 +++ b/lib/ur/monad.urs Sun Oct 17 13:26:11 2010 -0400 @@ -63,7 +63,5 @@ val appR2 : K --> m ::: (Type -> Type) -> monad m -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) - -> (nm :: Name -> t :: K -> rest :: {K} - -> [[nm] ~ rest] => - tf1 t -> tf2 t -> m unit) + -> (nm :: Name -> t :: K -> tf1 t -> tf2 t -> m unit) -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m unit