From 9569ae99c75cb74aeeb6fa02e6eec9eff2c7669f Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 23 Oct 2008 18:45:10 -0400 Subject: Crud2 demo --- lib/basis.urs | 3 ++- lib/top.ur | 2 ++ lib/top.urs | 2 ++ 3 files changed, 6 insertions(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/basis.urs b/lib/basis.urs index a8c81353..fce29ff9 100644 --- a/lib/basis.urs +++ b/lib/basis.urs @@ -18,6 +18,7 @@ val eq_int : eq int val eq_float : eq float val eq_string : eq string val eq_bool : eq bool +val mkEq : t ::: Type -> (t -> t -> bool) -> eq t class num val zero : t ::: Type -> num t -> t @@ -365,7 +366,7 @@ val radioOption : unit -> tag [Value = string] radio [] [] [] con select = [Select] val select : formTag string select [] -val option : unit -> tag [Value = string] select [] [] [] +val option : unit -> tag [Value = string, Selected = bool] select [] [] [] val submit : ctx ::: {Unit} -> use ::: {Type} -> fn [[Form] ~ ctx] => diff --git a/lib/top.ur b/lib/top.ur index 91cab991..0bc345de 100644 --- a/lib/top.ur +++ b/lib/top.ur @@ -1,3 +1,5 @@ +fun not b = if b then False else True + con idT (t :: Type) = t con record (t :: {Type}) = $t con fstTT (t :: (Type * Type)) = t.1 diff --git a/lib/top.urs b/lib/top.urs index 29a1acf1..22cebb16 100644 --- a/lib/top.urs +++ b/lib/top.urs @@ -1,3 +1,5 @@ +val not : bool -> bool + con idT = fn t :: Type => t con record = fn t :: {Type} => $t con fstTT = fn t :: (Type * Type) => t.1 -- cgit v1.2.3