Skip to content

Instantly share code, notes, and snippets.

@larrytheliquid larrytheliquid/VecIR.agda
Last active Feb 26, 2017

Embed
What would you like to do?
Generic representation: https://is.gd/rms0P7
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" ∷ []
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.