Mercurial > urweb

comparison lib/ur/top.ur @ 777:87a7702d681d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
outer demo
author Adam Chlipala <adamc@hcoop.net>
date Sun, 03 May 2009 14:57:33 -0400
parents acb8537f58f0
children d4e811beb8eb
comparison
equal deleted inserted replaced
776:9f2555f06901 777:87a7702d681d
69 f [choice] body 69 f [choice] body
70 70
71 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) 71 fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type)
72 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x) 72 (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x)
73 73
74 fun show_option (t ::: Type) (_ : show t) =
75 mkShow (fn opt : option t =>
76 case opt of
77 None => ""
78 | Some x => show x)
79
80 fun read_option (t ::: Type) (_ : read t) =
81 mkRead (fn s =>
82 case s of
83 "" => None
84 | _ => Some (readError s : t))
85 (fn s =>
86 case s of
87 "" => Some None
88 | _ => case read s of
89 None => None
90 | v => Some v)
91
74 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) = 92 fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) =
75 cdata (show v) 93 cdata (show v)
76 94
77 fun foldUR (tf :: Type) (tr :: {Unit} -> Type) 95 fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
78 (f : nm :: Name -> rest :: {Unit} 96 (f : nm :: Name -> rest :: {Unit}