Mercurial > urweb
diff lib/ur/top.ur @ 777:87a7702d681d
outer demo
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 03 May 2009 14:57:33 -0400 |
parents | acb8537f58f0 |
children | d4e811beb8eb |
line wrap: on
line diff
--- a/lib/ur/top.ur Sun May 03 12:49:47 2009 -0400 +++ b/lib/ur/top.ur Sun May 03 14:57:33 2009 -0400 @@ -71,6 +71,24 @@ 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)