matchless-tail.agda

module matchless-tail where

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

data Vec (A : Set) : ℕ → Set where
  nil : Vec A zero
  cons : ∀ {n} → A → Vec A n → Vec A (suc n)

ind-ℕ : (C : (n : ℕ) → Set)
      → C zero
      → ((n : ℕ) → C n → C (suc n))
      → (n : ℕ) → C n
ind-ℕ C base rec zero = base
ind-ℕ C base rec (suc n) = rec n (ind-ℕ _ base rec n)

sub1 : ℕ → ℕ
sub1 = ind-ℕ (λ _ → ℕ) zero (λ n _ → n)

ind : {A : Set}(C : (n : ℕ) → Vec A n → Set)
    → C zero nil
    → ({n : ℕ}(a : A)(v : Vec A n) → C n v → C (suc n) (cons a v))
    → {n : ℕ}(v : Vec A n) → C n v
ind C base rec nil = base
ind C base rec (cons x v) = rec x v (ind C base rec v)

P : {A : Set}(n : ℕ) → Vec A n → Set
P {A} n v = Vec A (sub1 n)

tail : {A : Set}{n : ℕ} → Vec A (suc n) → Vec A n
tail = ind P nil (λ _ v _ → v)