------------------------------------------------------------------------------------------------------------------------------------------- ( 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 ------------------------------------------------------------------------------------------------------------------------------------------- ( A, B : * ! let !-------------! ! Iff A B : * ) Iff A B => And (A -> B) (B -> A) ------------------------------------------------------------------------------------------------------------------------------------------- ( P : A -> * ! ( a : A ; p : P a ! data !------------! where !------------------! ! Ex P : * ) ! wit a p : Ex P ) ------------------------------------------------------------------------------------------------------------------------------------------- ( P : A -> * ! let !--------------------------------------------------------! ; allExLem [] ! allExLem : Iff (all a : A => (P a) -> Q) ((Ex P) -> Q) ) ------------------------------------------------------------------------------------------------------------------------------------------- data (----------! where (-------------! ; (--------------! ! Bool : * ) ! true : Bool ) ! false : Bool ) ------------------------------------------------------------------------------------------------------------------------------------------- [Define and to be the logical and (&&)] ------------------------------------------------------------------------------------------------------------------------------------------- ( b, c : Bool ! let !----------------! ! and b c : Bool ) and b c [] ------------------------------------------------------------------------------------------------------------------------------------------- ( b, c : Bool ! let !------------------------------------! ! andCom b c : (and b c) = (and c b) ) andCom b c [] ------------------------------------------------------------------------------------------------------------------------------------------- ( n : Nat ! data (---------! where (------------! ; !-------------! ! Nat : * ) ! zero : Nat ) ! suc n : Nat ) ------------------------------------------------------------------------------------------------------------------------------------------- let (-----------! ! one : Nat ) one => suc zero ------------------------------------------------------------------------------------------------------------------------------------------- let (-----------! ! two : Nat ) two => suc one ------------------------------------------------------------------------------------------------------------------------------------------- let (-------------! ! three : Nat ) three => suc two ------------------------------------------------------------------------------------------------------------------------------------------- ( m, n : Nat ! let !---------------! ! add m n : Nat ) add m n <= rec m { add m n <= case m { add zero n => n add (suc m) n => suc (add m n) } } ------------------------------------------------------------------------------------------------------------------------------------------- [minus should compute cut-off subtraction. If n>m them minus m n = 0 otherwise minus m n = m-n] ------------------------------------------------------------------------------------------------------------------------------------------- ( m, n : Nat ! let !-----------------! ! minus m n : Nat ) minus m n [] ------------------------------------------------------------------------------------------------------------------------------------------- inspect minus three two => ? : Nat ------------------------------------------------------------------------------------------------------------------------------------------- ( m, n : Nat ! let !--------------------------------------! ! minusLem m n : minus (add m n) m = n ) minusLem m n [] ------------------------------------------------------------------------------------------------------------------------------------------- [double m = 2*m] ------------------------------------------------------------------------------------------------------------------------------------------- ( m : Nat ! let !----------------! ! double m : Nat ) double m [] ------------------------------------------------------------------------------------------------------------------------------------------- inspect double three => ? : Nat ------------------------------------------------------------------------------------------------------------------------------------------- [half m = m/2, integer division by two.] ------------------------------------------------------------------------------------------------------------------------------------------- ( m : Nat ! let !--------------! ! half m : Nat ) half m [] ------------------------------------------------------------------------------------------------------------------------------------------- ( f : A -> B ; p : a = b ! let !-------------------------! ! resp f p : f a = f b ) resp f p <= case p { resp f refl => refl } ------------------------------------------------------------------------------------------------------------------------------------------- ( m : Nat ! let !---------------------------------------! ! halfDoubleLem m : half (double m) = m ) halfDoubleLem m [] ------------------------------------------------------------------------------------------------------------------------------------------- [min should calculate the minimum of two numbers.] ------------------------------------------------------------------------------------------------------------------------------------------- ( m, n : Nat ! let !---------------! ! min m n : Nat ) min m n [] ------------------------------------------------------------------------------------------------------------------------------------------- inspect min two three => ? : Nat ------------------------------------------------------------------------------------------------------------------------------------------- ( m, n : Nat ! let !--------------------------------! ! minCom m n : min m n = min n m ) minCom m n [] -------------------------------------------------------------------------------------------------------------------------------------------