summaryrefslogtreecommitdiff
path: root/lib/top.ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-12-19 10:27:58 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-12-19 10:27:58 -0500
commit3aac0d79c1ad2da6358cf6619c62a56ddd2ed195 (patch)
tree2ae9890ec2aaa8c2404ce09448a078fec7857bbb /lib/top.ur
parent55c83dd7bd3e7cefe40b70f3480dda746dc3384f (diff)
Monad type class seems to be working
Diffstat (limited to 'lib/top.ur')
-rw-r--r--lib/top.ur8
1 files changed, 4 insertions, 4 deletions
diff --git a/lib/top.ur b/lib/top.ur
index fd7676a3..35e8519b 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -30,8 +30,8 @@ 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 txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) =
- cdata (@show sh v)
+fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (_ : show t) (v : t) =
+ cdata (show v)
fun foldUR (tf :: Type) (tr :: {Unit} -> Type)
(f : nm :: Name -> rest :: {Unit}
@@ -233,9 +233,9 @@ fun eqNullable (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type})
(SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2})
fun eqNullable' (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type})
- (t ::: Type) (inj : sql_injectable (option t))
+ (t ::: Type) (_ : sql_injectable (option t))
(e1 : sql_exp tables agg exps (option t))
(e2 : option t) =
case e2 of
None => (SQL {e1} IS NULL)
- | Some _ => sql_binary sql_eq e1 (@sql_inject inj e2)
+ | Some _ => sql_binary sql_eq e1 (sql_inject e2)