From: Anders Mörtberg <mortberg@chalmers.se>
Date: Tue, 14 Apr 2015 21:04:00 +0000 (+0200)
Subject: Make list compile
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=e805638580e9fef033bdac631bf34f988681d60f;p=cubicaltt.git

Make list compile
---

diff --git a/examples/list.ctt b/examples/list.ctt
index 1073d10..64584a4 100644
--- a/examples/list.ctt
+++ b/examples/list.ctt
@@ -1,9 +1,11 @@
 module list where
 
+import prelude
+
 data list (A : U) = nil | cons (a : A) (as : list A)
 
 append (A : U) : list A -> list A -> list A = split
-  nil -> id (list A)
+  nil -> idfun (list A)
   cons x xs -> \(ys : list A) -> cons x (append A xs ys)
 
 reverse (A : U) : list A -> list A = split