comparison lib/ur/monad.ur @ 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
92 return ({nm = p'.1} ++ p.1, p'.2)) 92 return ({nm = p'.1} ++ p.1, p'.2))
93 (fn _ => return ({}, i)) 93 (fn _ => return ({}, i))
94 fl 94 fl
95 95
96 fun appR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] 96 fun appR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type]
97 (f : nm :: Name -> t :: K -> rest :: {K} 97 (f : nm :: Name -> t :: K -> tf1 t -> tf2 t -> m unit)
98 -> [[nm] ~ rest] =>
99 tf1 t -> tf2 t -> m unit)
100 [r ::: {K}] (fl : folder r) = 98 [r ::: {K}] (fl : folder r) =
101 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m unit] 99 @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m unit]
102 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 => 100 (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] acc r1 r2 =>
103 acc (r1 -- nm) (r2 -- nm); 101 acc (r1 -- nm) (r2 -- nm);
104 f [nm] [t] [rest] ! r1.nm r2.nm) 102 f [nm] [t] r1.nm r2.nm)
105 (fn _ _ => return ()) 103 (fn _ _ => return ())
106 fl 104 fl