Generic representation: https://is.gd/rms0P7

VecIR.agda

open import Data.Nat
open import Data.Product
open import Data.String
open import Relation.Binary.PropositionalEquality
module _ where

mutual
  data Vec₁ (A : Set) : Set where
    nil : Vec₁ A
    cons : (n : ℕ) → A → (xs : Vec₁ A) → Vec₂ xs ≡ n → Vec₁ A

  Vec₂ : {A : Set} → Vec₁ A → ℕ
  Vec₂ nil = zero
  Vec₂ (cons n x xs q) = suc (Vec₂ xs)

Vec : Set → ℕ → Set
Vec A n = Σ (Vec₁ A) (λ xs → Vec₂ xs ≡ n)

[] : {A : Set} → Vec A zero
[] = nil , refl

infixr 5 _∷_
_∷_ : {A : Set} {n : ℕ} → A → (xs : Vec A n) → Vec A (suc n)
x ∷ (xs , q) = cons _ x xs q , cong suc q

eg : Vec String 3
eg = "a" ∷ "b" ∷ "c" ∷ []