From e1618fb012b5926889d80893c9ac4ce08838519d Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 3 May 2009 14:57:33 -0400 Subject: outer demo --- lib/ur/top.ur | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'lib/ur/top.ur') diff --git a/lib/ur/top.ur b/lib/ur/top.ur index b9728158..f9b3d033 100644 --- a/lib/ur/top.ur +++ b/lib/ur/top.ur @@ -71,6 +71,24 @@ fun ex (tf :: (Type -> Type)) (choice :: Type) (body : tf choice) : ex tf = fun compose (t1 ::: Type) (t2 ::: Type) (t3 ::: Type) (f1 : t2 -> t3) (f2 : t1 -> t2) (x : t1) = f1 (f2 x) +fun show_option (t ::: Type) (_ : show t) = + mkShow (fn opt : option t => + case opt of + None => "" + | Some x => show x) + +fun read_option (t ::: Type) (_ : read t) = + mkRead (fn s => + case s of + "" => None + | _ => Some (readError s : t)) + (fn s => + case s of + "" => Some None + | _ => case read s of + None => None + | v => Some v) + fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) = cdata (show v) -- cgit v1.2.3