Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
open import Data.Nat
open import Data.Fin renaming ( zero to here ; suc to there )
open import Data.Product
open import Relation.Binary.PropositionalEquality
module _ where
data Vec₁ (A : Set) : Set where
nil₁ : Vec₁ A zero
cons₁ : {n : ℕ} A (xs : Vec₁ A n) toℕ (Vec₂ xs) ≡ n Vec₁ A (suc n)
Vec₂ : {A : Set}{n : ℕ} Vec₁ A n Fin (suc n)
Vec₂ nil₁ = here
Vec₂ (cons₁ x xs q) = there (Vec₂ xs)
Vec : Set Set
Vec A n = Σ (Vec₁ A n) (λ xs toℕ (Vec₂ xs) ≡ n)
nil : {A : Set} Vec A zero
nil = nil₁ , refl
cons : {A : Set} {n : ℕ} A Vec A n Vec A (suc n)
cons x (xs , q) = cons₁ x xs q , cong suc q
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.