Skip to content

Instantly share code, notes, and snippets.

@jozefg
Created October 17, 2018 12:17
Show Gist options
  • Save jozefg/82b6c2537d12ba8731668c234bd7ce81 to your computer and use it in GitHub Desktop.
Save jozefg/82b6c2537d12ba8731668c234bd7ce81 to your computer and use it in GitHub Desktop.
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment