--------------------------------------------------------------------------------------- ( A, B : * ! ( a : A ; b : B ! data !-------------! where !--------------------! ! And A B : * ) ! pair a b : And A B ) --------------------------------------------------------------------------------------- ( A, B : * ! ( a : A ! ( b : B ! data !------------! where !-----------------! ; !------------------! ! Or A B : * ) ! left a : Or A B ) ! right b : Or A B ) --------------------------------------------------------------------------------------- ( A : * ! let !-----------! ! Not A : * ) Not A => A -> Zero --------------------------------------------------------------------------------------- ( p : And A B ! let !-------------! ! fst p : A ) fst p <= case p { fst (pair a b) => a } --------------------------------------------------------------------------------------- ( p : And A B ! let !-------------! ! snd p : B ) snd p <= case p { snd (pair a b) => b } --------------------------------------------------------------------------------------- ( X : * ; P, Q : X -> * ; p : all x : X => And (P x) (Q x) ! let !------------------------------------------------------------! ! allAndLem p : And (all x : X => P x) (all x : X => Q x) ) allAndLem p => pair (lam x => fst (p x)) (lam x => snd (p x)) --------------------------------------------------------------------------------------- ( X : * ; P, Q : X -> * ! let !-------------------------------------------------------------------------------! ! allAndLem' : ! ! (all x : X => And (P x) (Q x)) -> And (all x : X => P x) (all x : X => Q x) ) allAndLem' => allAndLem --------------------------------------------------------------------------------------- ( X : * ; P, Q : X -> * ; q : And (all x : X => P x) (all x : X => Q x) ! let !-------------------------------------------------------------------------! ! andAllLem q : all x : X => And (P x) (Q x) ) andAllLem q <= case q { andAllLem (pair a b) => lam x => pair (a x) (b x) } --------------------------------------------------------------------------------------- data (----------! where (-------------! ; (--------------! ! Bool : * ) ! true : Bool ) ! false : Bool ) --------------------------------------------------------------------------------------- ( b : Bool ! let !--------------! ! not b : Bool ) not b <= case b { not true => false not false => true } --------------------------------------------------------------------------------------- inspect not true => false : Bool --------------------------------------------------------------------------------------- inspect not (not true) => true : Bool --------------------------------------------------------------------------------------- ( A : * ; a, b : A ! data !-------------------! where (----------------! ! Eq a b : * ) ! refl' : Eq a a ) --------------------------------------------------------------------------------------- ( b : Bool ! let !----------------------------------! ! notnotLem b : Eq (not (not b)) b ) notnotLem b <= case b { notnotLem true => refl' notnotLem false => refl' } --------------------------------------------------------------------------------------- ( A : * ; a, b : A ; p : Eq a b ! let !---------------------------------! ! sym p : Eq b a ) sym p <= case p { sym refl' => refl' } --------------------------------------------------------------------------------------- ( p : Eq a b ; q : Eq b c ! let !--------------------------! ! trans p q : Eq a c ) trans p q <= case p { trans refl' q => q } --------------------------------------------------------------------------------------- ( p : true = false ! let !------------------! ! tnef p : Zero ) tnef p <= case p --------------------------------------------------------------------------------------- ( f : A -> B ; p : a = b ! let !-------------------------! ! resp f p : f a = f b ) resp f p <= case p { resp f refl => refl } --------------------------------------------------------------------------------------- ( f : A -> B ; p : f a = f b ! let !-----------------------------! ! garbage f p : a = b ) garbage f p <= case p { garbage f p [] } ---------------------------------------------------------------------------------------