diff options
Diffstat (limited to 'itt.ka')
-rw-r--r-- | itt.ka | 34 |
1 files changed, 34 insertions, 0 deletions
@@ -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 × + |