2 files changed, 30 insertions, 0 deletions
diff --git a/test/c/list.expect b/test/c/list.expect
new file mode 100644
index 00000000..e6bdb2f8
--- /dev/null
+++ b/test/c/list.expect
@@ -0,0 +1,3 @@
+y = 1
+hd(tl(x)) = 2
+hd(tl(tl(x))) = 3
diff --git a/test/c/list.sail b/test/c/list.sail
new file mode 100644
index 00000000..c315d3bf
--- /dev/null
+++ b/test/c/list.sail
@@ -0,0 +1,27 @@
+
+val "print_int" : (string, int) -> unit
+
+val hd : forall ('a : Type). ('a, list('a)) -> 'a
+
+function hd (def, xs) =
+  match xs {
+    y :: ys => y,
+    [||]    => def
+  }
+
+val tl : forall ('a : Type). list('a) -> list('a)
+
+function tl xs = match xs {
+    y :: ys => ys,
+    [||]    => [||]
+  }
+
+val main : unit -> unit
+
+function main () = {
+  let x : list(int) = [|1, 2, 3|];
+  let y = hd(0 : int, x);
+  print_int("y = ", y);
+  print_int("hd(tl(x)) = ", hd(0, tl(x)));
+  print_int("hd(tl(tl(x))) = ", hd(0, tl(tl(x))));
+}
+\ No newline at end of file