--------------------------------------------------------------------------------------- [] --------------------------------------------------------------------------------------- ( A, B : * ! ( a : A ! ( b : B ! data !------------! where !-----------------! ; !------------------! ! Or A B : * ) ! left a : Or A B ) ! right b : Or A B ) --------------------------------------------------------------------------------------- ( A, B : * ! ( a : A ; b : B ! data !-------------! where !--------------------! ! And A B : * ) ! pair a b : And A B ) --------------------------------------------------------------------------------------- ( A : * ! let !-----------! ! Not A : * ) Not A => A -> Zero --------------------------------------------------------------------------------------- ( 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) } } --------------------------------------------------------------------------------------- ( a, b : A ; p : a = b ! let !-----------------------! ! eqSym p : b = a ) eqSym p <= case p { eqSym refl => refl } --------------------------------------------------------------------------------------- ( a, b, c : A ; p : a = b ; q : b = c ! let !---------------------------------------! ! eqTrans p q : a = c ) eqTrans p q <= case p { eqTrans refl q => q } --------------------------------------------------------------------------------------- ( f : A -> B ; p : a = b ! let !----------------------------! ! eqResp f p : (f a) = (f b) ) eqResp f p <= case p { eqResp f refl => refl } --------------------------------------------------------------------------------------- ( f : A -> B -> C ; p : a = b ; q : c = d ! let !-------------------------------------------! ! eqResp2 f p q : f a c = f b d ) eqResp2 f p q <= case p { eqResp2 f refl q <= case q { eqResp2 f refl refl => refl } } --------------------------------------------------------------------------------------- ( P : A -> * ; a, b : A ; q : a = b ; p : P a ! let !------------------------------------------------! ! eqSubst q p : P b ) eqSubst q p <= case q { eqSubst refl p => p } --------------------------------------------------------------------------------------- ( A : * ! ( a : A ; as : List A ! data !------------! where (--------------! ; !----------------------! ! List A : * ) ! nil : List A ) ! cons a as : List A ) --------------------------------------------------------------------------------------- let (-----------------! ! l123 : List Nat ) l123 => cons one (cons two (cons three nil)) --------------------------------------------------------------------------------------- ( as, bs : List A ! let !-----------------------! ! append as bs : List A ) append as bs <= rec as { append as bs <= case as { append nil bs => bs append (cons a as) bs => cons a (append as bs) } } --------------------------------------------------------------------------------------- inspect append l123 l123 => cons (suc zero) (cons (suc (suc zero)) ! : List Nat !% (cons (suc (suc (suc zero))) !! ! !% (cons (suc zero) !!! ! ! !% (cons (suc (suc zero)) !!!! ! ! ! !% (cons (suc (suc (suc zero))) nil))))) --------------------------------------------------------------------------------------- ( as : List A ! let !-----------------! ! rev as : List A ) rev as <= rec as { rev as <= case as { rev nil => nil rev (cons a as) => append (rev as) (cons a nil) } } --------------------------------------------------------------------------------------- inspect rev l123 => cons (suc (suc (suc zero))) (cons (suc (suc zero)) (cons (suc zero) nil)) : List Nat --------------------------------------------------------------------------------------- inspect rev (rev l123) => cons (suc zero) (cons (suc (suc zero)) ! : List Nat !% (cons (suc (suc (suc zero))) nil)) --------------------------------------------------------------------------------------- ( a : A ; as : List A ! let !--------------------------------------------------------------! ! revlem a as : rev (append as (cons a nil)) = cons a (rev as) ) revlem a as <= rec as { revlem a as <= case as { revlem a nil => refl revlem a' (cons a as) => eqResp (lam xs => append xs (cons a nil)) (revlem a' as) } } --------------------------------------------------------------------------------------- ( as : List A ! let !-------------------------------! ! revrev as : rev (rev as) = as ) revrev as <= rec as { revrev as <= case as { revrev nil => refl revrev (cons a as) => eqTrans (revlem a (rev as)) (eqResp (cons a) (revrev as)) } } --------------------------------------------------------------------------------------- ( as : List A ! let !-------------! ! hd as : A ) hd as <= case as { hd nil [] hd (cons a as) => a } --------------------------------------------------------------------------------------- ( A : * ! ( a : A ! data !-------------! where !----------------! ; (-----------------! ! Error A : * ) ! ok a : Error A ) ! error : Error A ) --------------------------------------------------------------------------------------- ( as : List A ! let !------------------! ! hd' as : Error A ) hd' as <= case as { hd' nil => error hd' (cons a as) => ok a } --------------------------------------------------------------------------------------- inspect hd' l123 => ok (suc zero) : Error Nat --------------------------------------------------------------------------------------- inspect hd' nil => error : Error ? --------------------------------------------------------------------------------------- ( n : Nat ; A : * ! ( a : A ; as : Vec n A ! data !------------------! where (--------------! ; !-----------------------! ! Vec n A : * ) ! vnil : ! ! vcons a as : ! ! Vec zero A ) ! Vec (suc n) A ) --------------------------------------------------------------------------------------- let (----------------------! ! v123 : Vec three Nat ) v123 => vcons one (vcons two (vcons three vnil)) --------------------------------------------------------------------------------------- ( v : Vec (suc n) A ! let !-------------------! ! vhd v : A ) vhd v <= case v { vhd (vcons a av) => a } --------------------------------------------------------------------------------------- inspect vhd v123 => suc zero : Nat --------------------------------------------------------------------------------------- inspect vhd vnil => ? : ? --------------------------------------------------------------------------------------- ( as : Vec n A ; bs : Vec m A ! let !---------------------------------! ! vappend as bs : Vec (add n m) A ) vappend as bs <= rec as { vappend as bs <= case as { vappend vnil bs => bs vappend (vcons a as) bs => vcons a (vappend as bs) } } --------------------------------------------------------------------------------------- inspect vappend v123 v123 => vcons (suc zero) (vcons (suc (suc zero)) ! !% (vcons (suc (suc (suc zero))) !! ! !% (vcons (suc zero) !!! ! ! !% (vcons (suc (suc zero)) !!!! ! ! ! !% (vcons (suc (suc (suc zero))) vnil))))) : Vec (suc (suc (suc (suc (suc (suc zero)))))) Nat --------------------------------------------------------------------------------------- ( n : Nat ! ( i : Fin n ! data !-----------! where (------------------! ; !--------------------! ! Fin n : * ) ! fz : Fin (suc n) ) ! fs i : Fin (suc n) ) --------------------------------------------------------------------------------------- ( n : Nat ! let !---------------------! ! max n : Fin (suc n) ) max n <= rec n { max n <= case n { max zero => fz max (suc n) => fs (max n) } } --------------------------------------------------------------------------------------- inspect max two => fs (fs fz) : Fin (suc (suc (suc zero))) --------------------------------------------------------------------------------------- inspect fz => fz : Fin (suc ?) --------------------------------------------------------------------------------------- inspect fz _ one => fz : Fin (suc (suc zero)) --------------------------------------------------------------------------------------- inspect fs fz => fs fz : Fin (suc (suc ?)) --------------------------------------------------------------------------------------- inspect fs [] => fs ? : Fin (suc ?) --------------------------------------------------------------------------------------- ( as : Vec n A ; i : Fin n ! let !---------------------------! ! vnth as i : A ) vnth as i <= rec as { vnth as i <= case as { vnth vnil i <= case i vnth (vcons a as) i <= case i { vnth (vcons a as) fz => a vnth (vcons a as) (fs i) => vnth as i } } } --------------------------------------------------------------------------------------- inspect vnth v123 (fs fz) => suc (suc zero) : Nat --------------------------------------------------------------------------------------- ( as : Vec n A ; i : Fin n ! let !---------------------------! ! vnth' as i : A ) vnth' as i <= rec as { vnth' as i <= case i { vnth' as fz <= case as { vnth' (vcons a as) fz => a } vnth' as (fs i) <= case as { vnth' (vcons a as) (fs i) => vnth' as i } } } --------------------------------------------------------------------------------------- ( as : Vec n A ; a : A ! let !----------------------------! ! vsnoc as a : Vec (suc n) A ) vsnoc as a <= rec as { vsnoc as a <= case as { vsnoc vnil a => vcons a vnil vsnoc (vcons a as) a' => vcons a (vsnoc as a') } } --------------------------------------------------------------------------------------- ( as : Vec n A ! let !-------------------! ! vrev as : Vec n A ) vrev as <= rec as { vrev as <= case as { vrev vnil => vnil vrev (vcons a as) => vsnoc (vrev as) a } } ---------------------------------------------------------------------------------------