Mercurial > urweb

comparison lib/top.ur @ 403:8084fa9216de

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New implicit argument handling
author Adam Chlipala <adamc@hcoop.net>
date Tue, 21 Oct 2008 16:41:11 -0400
parents 28d3d7210687
children 06fcddcd20d3
comparison
equal deleted inserted replaced
402:ebf27030ae3b 403:8084fa9216de
18 18
19 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) 19 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type)
20 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x) 20 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
21 21
22 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = 22 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) =
23 cdata (show sh v) 23 cdata (@show sh v)
24 24
25 fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type) 25 fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
26 (f : nm :: Name -> t :: Type -> rest :: {Type} 26 (f : nm :: Name -> t :: Type -> rest :: {Type}
27 -> fn [[nm] ~ rest] => 27 -> fn [[nm] ~ rest] =>
28 tf t -> tr rest -> tr ([nm = t] ++ rest)) 28 tf t -> tr rest -> tr ([nm = t] ++ rest))