Mercurial > urweb
comparison lib/top.ur @ 403:8084fa9216de
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)) |