comparison lib/ur/top.urs @ 937:37dd42935dad

Summary row with aggregates
author Adam Chlipala <adamc@hcoop.net>
date Tue, 15 Sep 2009 10:18:56 -0400
parents 8e540df3294d
children 10114d7b7477
comparison
equal deleted inserted replaced
936:6966d98c80b5 937:37dd42935dad
46 -> xml ctx use [] 46 -> xml ctx use []
47 47
48 val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) 48 val mp : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type)
49 -> (t ::: K -> tf1 t -> tf2 t) 49 -> (t ::: K -> tf1 t -> tf2 t)
50 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) 50 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r)
51 val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) 51 val map2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf :: (K -> Type)
52 -> (t ::: K -> tf1 t -> tf2 t -> tf3 t) 52 -> (t ::: K -> tf1 t -> tf2 t -> tf t)
53 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) 53 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf r)
54 val map3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) -> tf :: (K -> Type)
55 -> (t ::: K -> tf1 t -> tf2 t -> tf3 t -> tf t)
56 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> $(map tf r)
54 57
55 val foldUR : tf :: Type -> tr :: ({Unit} -> Type) 58 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
56 -> (nm :: Name -> rest :: {Unit} 59 -> (nm :: Name -> rest :: {Unit}
57 -> [[nm] ~ rest] => 60 -> [[nm] ~ rest] =>
58 tf -> tr rest -> tr ([nm] ++ rest)) 61 tf -> tr rest -> tr ([nm] ++ rest))