summaryrefslogtreecommitdiff
path: root/lib/ur/list.ur
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-28 12:40:55 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-28 12:40:55 -0400
commit8327f190c80287003048eaa10857d0f081b551bb (patch)
tree1ebd4c0f5a8f22a6ddd0dbb86cd2cc741b610e0e /lib/ur/list.ur
parenta735f6ea0ef8ec5895dfe7f895f89ee8c126de14 (diff)
Fix EDLet elab_util bug
Diffstat (limited to 'lib/ur/list.ur')
-rw-r--r--lib/ur/list.ur70
1 files changed, 35 insertions, 35 deletions
diff --git a/lib/ur/list.ur b/lib/ur/list.ur
index 90729f5c..8493f2f5 100644
--- a/lib/ur/list.ur
+++ b/lib/ur/list.ur
@@ -1,38 +1,38 @@
datatype t = datatype Basis.list
-val show (a ::: Type) (_ : show a) =
- let
- fun show' (ls : list a) =
- case ls of
- [] => "[]"
- | x :: ls => show x ^ " :: " ^ show' ls
- in
- mkShow show'
- end
+val show = fn [a] (_ : show a) =>
+ let
+ fun show' (ls : list a) =
+ case ls of
+ [] => "[]"
+ | x :: ls => show x ^ " :: " ^ show' ls
+ in
+ mkShow show'
+ end
-val rev (a ::: Type) =
- let
- fun rev' acc (ls : list a) =
- case ls of
- [] => acc
- | x :: ls => rev' (x :: acc) ls
- in
- rev' []
- end
+val rev = fn [a] =>
+ let
+ fun rev' acc (ls : list a) =
+ case ls of
+ [] => acc
+ | x :: ls => rev' (x :: acc) ls
+ in
+ rev' []
+ end
-val revAppend (a ::: Type) =
- let
- fun ra (ls : list a) acc =
- case ls of
- [] => acc
- | x :: ls => ra ls (x :: acc)
- in
- ra
- end
+val revAppend = fn [a] =>
+ let
+ fun ra (ls : list a) acc =
+ case ls of
+ [] => acc
+ | x :: ls => ra ls (x :: acc)
+ in
+ ra
+ end
-fun append (a ::: Type) (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
+fun append [a] (ls1 : t a) (ls2 : t a) = revAppend (rev ls1) ls2
-fun mp (a ::: Type) (b ::: Type) f =
+fun mp [a] [b] f =
let
fun mp' acc ls =
case ls of
@@ -42,7 +42,7 @@ fun mp (a ::: Type) (b ::: Type) f =
mp' []
end
-fun mapPartial (a ::: Type) (b ::: Type) f =
+fun mapPartial [a] [b] f =
let
fun mp' acc ls =
case ls of
@@ -54,7 +54,7 @@ fun mapPartial (a ::: Type) (b ::: Type) f =
mp' []
end
-fun mapX (a ::: Type) (ctx ::: {Unit}) f =
+fun mapX [a] [ctx ::: {Unit}] f =
let
fun mapX' ls =
case ls of
@@ -64,7 +64,7 @@ fun mapX (a ::: Type) (ctx ::: {Unit}) f =
mapX'
end
-fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f =
+fun mapM [m ::: (Type -> Type)] (_ : monad m) [a] [b] f =
let
fun mapM' acc ls =
case ls of
@@ -74,7 +74,7 @@ fun mapM (m ::: (Type -> Type)) (_ : monad m) (a ::: Type) (b ::: Type) f =
mapM' []
end
-fun filter (a ::: Type) f =
+fun filter [a] f =
let
fun fil acc ls =
case ls of
@@ -84,7 +84,7 @@ fun filter (a ::: Type) f =
fil []
end
-fun exists (a ::: Type) f =
+fun exists [a] f =
let
fun ex ls =
case ls of
@@ -98,7 +98,7 @@ fun exists (a ::: Type) f =
ex
end
-fun foldlMap (a ::: Type) (b ::: Type) (c ::: Type) f =
+fun foldlMap [a] [b] [c] f =
let
fun fold ls' st ls =
case ls of