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