comparison lib/top.urs @ 336:34847732cefc

Crud gets column headings
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Sep 2008 20:04:28 -0400
parents 9601c717d2f3
children 075b36dbb1a4
comparison
equal deleted inserted replaced
335:bc5015b89dd2 336:34847732cefc
8 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3) 8 -> (t2 -> t3) -> (t1 -> t2) -> (t1 -> t3)
9 9
10 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t 10 val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
11 -> xml ctx use [] 11 -> xml ctx use []
12 12
13 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
14 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
15 -> tf t -> tr rest -> tr ([nm = t] ++ rest))
16 -> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r
17
13 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type) 18 val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type)
14 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 19 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
15 -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) 20 -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
16 -> tr [] -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r 21 -> tr [] -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r
22
23 val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
24 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
25 -> tf t -> xml ctx [] [])
26 -> r :: {Type} -> $(mapTT tf r) -> xml ctx [] []
17 27
18 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} 28 val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
19 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest 29 -> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
20 -> tf1 t -> tf2 t -> xml ctx [] []) 30 -> tf1 t -> tf2 t -> xml ctx [] [])
21 -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] [] 31 -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] []