Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Product
module _ where
----------------------------------------------------------------------
data Desc (I : Set) : Set₁ where
: I Desc I
: I Desc I Desc I
: (A : Set) (D : A Desc I) Desc I
⟦_⟧ : {I : Set} (D : Desc I) (X : I Set) Set
⟦ `ι i ⟧ X =
⟦ `δ i D ⟧ X = X i × ⟦ D ⟧ X
⟦ `σ A D ⟧ X = Σ A λ a ⟦ D a ⟧ X
idx : {I : Set} (D : Desc I) (X : I Set) (xs : ⟦ D ⟧ X) I
idx (`ι i) X u = i
idx (`δ i D) X (x , xs) = idx D X xs
idx (`σ A D) X (a , xs) = idx (D a) X xs
data μ {I : Set} (D : Desc I) : I Set where
init : (xs : ⟦ D ⟧ (μ D)) μ D (idx D (μ D) xs)
----------------------------------------------------------------------
module PropVec where
VecD : Set Desc ℕ
VecD A = `σ Bool λ b if b
then `ι zero
else `σ ℕ λ n `σ A λ _ `δ n (`ι (suc n))
Vec : Set Set
Vec A n = μ (VecD A) n
nil : (A : Set) Vec A zero
nil A = init (true , tt)
cons : (A : Set) (n : ℕ) A Vec A n Vec A (suc n)
cons A n a xs = init (false , n , a , xs , tt)
-- idx
-- (if proj₁ xs then `ι zero else
-- `σ ℕ (λ n → `σ A (λ _ → `δ n (`ι (suc n)))))
-- (μ (VecD A)) (proj₂ xs)
-- != suc n of type ℕ
-- when checking that the pattern init (false , n , a , ys , tt) has
-- type μ (VecD A) (suc n)
tail : {A : Set} {n : ℕ} Vec A (suc n) Vec A n
tail (init (false , n , a , ys , tt)) = ys
----------------------------------------------------------------------
open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality
module _ where
----------------------------------------------------------------------
data Desc (I : Set) : Set₁ where
: I Desc I
: I Desc I Desc I
: (A : Set) (D : A Desc I) Desc I
⟦_⟧ : {I : Set} (D : Desc I) (X : I Set) Set
⟦ `ι i ⟧ X =
⟦ `δ i D ⟧ X = X i × ⟦ D ⟧ X
⟦ `σ A D ⟧ X = Σ A λ a ⟦ D a ⟧ X
idx : {I : Set} (D : Desc I) (X : I Set) (xs : ⟦ D ⟧ X) I
idx (`ι i) X u = i
idx (`δ i D) X (x , xs) = idx D X xs
idx (`σ A D) X (a , xs) = idx (D a) X xs
data μ {I : Set} (D : Desc I) (i : I) : Set where
init : (xs : ⟦ D ⟧ (μ D)) (q : idx D (μ D) xs ≡ i) μ D i
----------------------------------------------------------------------
module PropVec where
VecD : Set Desc ℕ
VecD A = `σ Bool λ b if b
then `ι zero
else `σ ℕ λ n `σ A λ _ `δ n (`ι (suc n))
Vec : Set Set
Vec A n = μ (VecD A) n
nil : (A : Set) Vec A zero
nil A = init (true , tt) refl
cons : (A : Set) (n : ℕ) A Vec A n Vec A (suc n)
cons A n a xs = init (false , n , a , xs , tt) refl
tail : {A : Set} {n : ℕ} Vec A (suc n) Vec A n
tail (init (true , xs) ())
tail (init (false , n , a , xs , tt) refl) = xs
----------------------------------------------------------------------
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.