Mercurial > urweb

comparison lib/top.urs @ 418:ad7e854a518c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Metaform demos, minus prose
author Adam Chlipala <adamc@hcoop.net>
date Thu, 23 Oct 2008 14:03:12 -0400
parents 06fcddcd20d3
children 0ce90d4d9ae7
comparison
equal deleted inserted replaced
417:e0e9e9eca1cb 418:ad7e854a518c
26 val foldUR : tf :: Type -> tr :: ({Unit} -> Type) 26 val foldUR : tf :: Type -> tr :: ({Unit} -> Type)
27 -> (nm :: Name -> rest :: {Unit} 27 -> (nm :: Name -> rest :: {Unit}
28 -> fn [[nm] ~ rest] => 28 -> fn [[nm] ~ rest] =>
29 tf -> tr rest -> tr ([nm] ++ rest)) 29 tf -> tr rest -> tr ([nm] ++ rest))
30 -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r 30 -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r
31
32 val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type)
33 -> (nm :: Name -> rest :: {Unit}
34 -> fn [[nm] ~ rest] =>
35 tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest))
36 -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r
37
38 val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit}
39 -> (nm :: Name -> rest :: {Unit}
40 -> fn [[nm] ~ rest] =>
41 tf1 -> tf2 -> xml ctx [] [])
42 -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] []
31 43
32 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) 44 val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
33 -> (nm :: Name -> t :: Type -> rest :: {Type} 45 -> (nm :: Name -> t :: Type -> rest :: {Type}
34 -> fn [[nm] ~ rest] => 46 -> fn [[nm] ~ rest] =>
35 tf t -> tr rest -> tr ([nm = t] ++ rest)) 47 tf t -> tr rest -> tr ([nm = t] ++ rest))