------------------------------------------------------------------------------------------------------------------------------------------- ( a, b, c : A ; p : a = b ; q : b = c ! let !---------------------------------------! ! trans p q : a = c ) trans p q <= case p { trans refl q => q } ------------------------------------------------------------------------------------------------------------------------------------------- ( f : A -> B ; p : a = b ! let !-------------------------! ! resp f p : f a = f b ) resp f p <= case p { resp f refl => refl } ------------------------------------------------------------------------------------------------------------------------------------------- data (----------! where (-------------! ; (--------------! ! Bool : * ) ! true : Bool ) ! false : Bool ) ------------------------------------------------------------------------------------------------------------------------------------------- ( 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 ------------------------------------------------------------------------------------------------------------------------------------------- ( x, y : Nat ! let !---------------! ! add x y : Nat ) add x y <= rec x { add x y <= case x { add zero y => y add (suc n) y => suc (add n y) } } ------------------------------------------------------------------------------------------------------------------------------------------- ( x, y : Nat ! let !----------------! ! mult x y : Nat ) mult x y <= rec x { mult x y <= case x { mult zero y => zero mult (suc x) y => add y (mult x y) } } ------------------------------------------------------------------------------------------------------------------------------------------- ( bs : Bin ; b : Bool ! data (---------! where (--------------! ; !----------------------! ! Bin : * ) ! bempty : Bin ) ! bext bs b : Bin ) ------------------------------------------------------------------------------------------------------------------------------------------- let (------------! ! bone : Bin ) bone [] ------------------------------------------------------------------------------------------------------------------------------------------- let (------------! ! bsix : Bin ) bsix [] ------------------------------------------------------------------------------------------------------------------------------------------- ( bs : Bin ! let !------------------! ! bin2nat bs : Nat ) bin2nat bs [] ------------------------------------------------------------------------------------------------------------------------------------------- inspect bin2nat bsix => ? : Nat ------------------------------------------------------------------------------------------------------------------------------------------- ( n : Nat ! let !-----------------! ! nat2bin n : Bin ) nat2bin n [] ------------------------------------------------------------------------------------------------------------------------------------------- ( n : Nat ! let !-----------------------------------------! ! nat2natProp n : bin2nat (nat2bin n) = n ) nat2natProp n [] ------------------------------------------------------------------------------------------------------------------------------------------- ( n : Nat ! data !------------! where [] ! Word n : * ) ------------------------------------------------------------------------------------------------------------------------------------------- ( w : Word n ! let !------------------! ; word2bin w [] ! word2bin w : Bin ) ------------------------------------------------------------------------------------------------------------------------------------------- ( bs : Bin ! let !-----------------------! ; ! bin2word bs : Word [] ) ------------------------------------------------------------------------------------------------------------------------------------------- ( w, w' : Word n ! let !--------------------------! ; wadd w w' [] ! wadd w w' : Word (suc n) ) -------------------------------------------------------------------------------------------------------------------------------------------