------------------------------------------------------------------------------
( x : Nat !
data Nat : * where zero : Nat ; !--------------!
! succ x : Nat )
------------------------------------------------------------------------------
( l : Nat ; t : * !
data !------------------!
! Vec l t : * )
( l : Nat ; t : * ; v : t ; vs : Vec l t !
where (--------------! ; !-------------------------------------------!
! vempty t : ! ! vcons l t v vs : Vec (succ l) t )
! Vec zero t )
------------------------------------------------------------------------------
( x : Nat ; y : Nat !
let !--------------------!
! add x y : Nat )
add x y <= case x
{ add zero y => y
add (succ x) y <= rec x
{ add (succ x) y => add x (succ y)
}
}
------------------------------------------------------------------------------
( l1 : Nat ; l2 : Nat ; t : * ; vs1 : Vec l1 t ; vs2 : Vec l2 t !
let !-------------------------------------------------------------------!
! vappend l1 l2 t vs1 vs2 : Vec (add l1 l2) t )
vappend l1 l2 t vs1 vs2 <= case vs1
{ vappend zero l2 t (vempty t) vs2 => vs2
vappend (succ l) l2 t (vcons l t v vs) vs2
=> vcons (add l l2) t v (vappend l l2 t vs vs2)
}
------------------------------------------------------------------------------