Fix imports

diff --git a/examples/bool.ctt b/examples/bool.ctt
index fea7111f8606be7876968b4c55d8b5e646547ff1..5688ea70ff630850e03d84a1f2225707e0ceff5b 100644 (file)
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -1,6 +1,6 @@
 module bool where
 
-import gradLemma
+import prelude
 
 data bool = false | true
 

diff --git a/examples/int.ctt b/examples/int.ctt
index 46f14ce8f9c941f3bdcba98d9c6ac28def4d66ae..16e8e5e69bf0710e69db41e17aabc29b3ef4df90 100644 (file)
--- a/examples/int.ctt
+++ b/examples/int.ctt
@@ -2,7 +2,6 @@ module int where
 \r
 import nat\r
 import discor\r
-import gradLemma\r
 \r
        ---------------------------------------------------\r
        -- Example: Non-trivial equality between Z and Z --\r

diff --git a/examples/pi.ctt b/examples/pi.ctt
index ef82c8ca5c8c3c7044715d1b432613eef73e0d26..2f1369bcd3c6730acb5c42ccc43c1ebea7f4a3eb 100644 (file)
--- a/examples/pi.ctt
+++ b/examples/pi.ctt
@@ -1,6 +1,6 @@
 module pi where
 
-import gradLemma
+import prelude
 
               -----------------------------------
               -- Example: Equality in pi types --