module VecDrop where data Nat : Set where zero : Nat suc : Nat -> Nat data Vect (A : Set) : Nat -> Set where vnil : Vect A zero vcons : {n : Nat} -> A -> Vect A n -> Vect A (suc n) {- Exercise: Define drop function for vectors -} _-_ : Nat -> Nat -> Nat zero - m = zero (suc n) - (suc m) = n - m (suc n) - zero = suc n drop : {A : Set}{n : Nat}(m : Nat) -> Vect A n -> Vect A (n - m) drop m vnil = vnil drop zero (vcons x xs) = vcons x xs drop (suc m) (vcons x xs) = drop m xs