From 4960cd8c2ec1e02c90e42d16db13f045427b4173 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 9 Sep 2008 11:46:33 -0400
Subject: Termination checking

---
 tests/termination.ur | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 tests/termination.ur

(limited to 'tests/termination.ur')

diff --git a/tests/termination.ur b/tests/termination.ur
new file mode 100644
index 00000000..64acd996
--- /dev/null
+++ b/tests/termination.ur
@@ -0,0 +1,28 @@
+datatype list a = Nil | Cons of a * list a
+
+fun isNil (t ::: Type) (ls : list t) : bool =
+        case ls of
+          Nil => True
+        | Cons _ => False
+
+fun append (t ::: Type) (ls1 : list t) (ls2 : list t) : list t =
+        case ls1 of
+          Nil => ls2
+        | Cons (x, ls1') => Cons (x, append ls1' ls2)
+
+fun appendR (t ::: Type) (ls2 : list t) (ls1 : list t) : list t =
+        case ls1 of
+          Nil => ls2
+        | Cons (x, ls1') => Cons (x, appendR ls2 ls1')
+
+(*fun naughty (t ::: Type) (ls : list t) : list t = naughty ls*)
+
+fun append1 (t ::: Type) (ls1 : list t) (ls2 : list t) : list t =
+        case ls1 of
+          Nil => ls2
+        | Cons (x, ls1') => Cons (x, append2 ls2 ls1')
+
+and append2 (t ::: Type) (ls2 : list t) (ls1 : list t) : list t =
+        case ls1 of
+          Nil => ls2
+        | Cons (x, ls1') => Cons (x, append1 ls1' ls2)
-- 
cgit v1.2.3