more report

[bitonic-mengthesis.git] / itt.ka

diff --git a/itt.ka b/itt.ka
index e9decf6bb4a19d72bdfd3de644adc9827246afa4..3f81a4549bde4adefb3a5eda972ec4fe0ca9d8b1 100644 (file)
--- a/itt.ka
+++ b/itt.ka
@@ -1,3 +1,6 @@
+------------------------------------------------------------
+-- Core ITT (minus W)
+
 data Empty : * => { }
 
 absurd [A : *] [x : Empty] : A => (
@@ -15,3 +18,34 @@ data Bool : * => { true : Bool | false : Bool }
 
 -- The if_then_else_ is provided by Bool-Elim
 
+------------------------------------------------------------
+-- Examples →
+
+data Nat : * => { zero : Nat | suc : Nat -> Nat }
+
+gt [n : Nat] : Nat -> * => (
+  Nat-Elim
+    n
+    (\_ => Nat -> *)
+    (\_ => Empty)
+    (\n f m => Nat-Elim m (\_ => *) Unit (\m' _ => f m'))
+)
+
+data List : [A : *] -> * =>
+  { nil : List A | cons : A -> List A -> List A }
+
+length [A : *] [xs : List A] : Nat => (
+    List-Elim xs (\_ => Nat) zero (\_ _ n => suc n)
+)
+
+head [A : *] [xs : List A] : gt (length A xs) zero -> A => (
+    List-Elim
+      xs
+      (\xs => gt (length A xs) zero -> A)
+      (\p => absurd A p)
+      (\x _ _ _ => x)
+)
+
+------------------------------------------------------------
+-- Examples ×
+