1 ------------------------------------------------------------
6 absurd [A : *] [x : Empty] : A => (
10 neg [A : *] : * => (A -> Empty)
12 record Unit : * => tt { }
14 record Prod : [A : *] [B : A -> *] -> * =>
15 prod {fst : A, snd : B fst}
17 data Bool : * => { true : Bool | false : Bool }
19 -- The if_then_else_ is provided by Bool-Elim
21 ------------------------------------------------------------
24 data Nat : * => { zero : Nat | suc : Nat -> Nat }
26 gt [n : Nat] : Nat -> * => (
31 (\n f m => Nat-Elim m (\_ => *) Unit (\m' _ => f m'))
34 data List : [A : *] -> * =>
35 { nil : List A | cons : A -> List A -> List A }
37 length [A : *] [xs : List A] : Nat => (
38 List-Elim xs (\_ => Nat) zero (\_ _ n => suc n)
41 head [A : *] [xs : List A] : gt (length A xs) zero -> A => (
44 (\xs => gt (length A xs) zero -> A)
49 ------------------------------------------------------------