From a95622ca33a31a8c6d3cb31c7ca3b390e7aa5624 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 24 Mar 2021 09:30:13 +0000
Subject: Begin soundness proof.

---
 src/Cfe/Context/Base.agda | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'src/Cfe/Context')

diff --git a/src/Cfe/Context/Base.agda b/src/Cfe/Context/Base.agda
index 6b34a67..2814a64 100644
--- a/src/Cfe/Context/Base.agda
+++ b/src/Cfe/Context/Base.agda
@@ -54,6 +54,11 @@ record Context n : Set (c ⊔ lsuc ℓ) where
     Γ : Vec (Type ℓ ℓ) (n ∸ m)
     Δ : Vec (Type ℓ ℓ) m
 
+
+toVec : ∀ {n} → Context n → Vec (Type ℓ ℓ) n
+toVec record { m = .0 ; m≤n = _ ; Γ = Γ ; Δ = [] } = Γ
+toVec {suc n} record { m = .(suc _) ; m≤n = (s≤s m≤n) ; Γ = Γ ; Δ = (x ∷ Δ) } = x ∷ toVec (record { m≤n = m≤n ; Γ = Γ ; Δ = Δ })
+
 wkn₁ : ∀ {n i} → (Γ,Δ : Context n) → toℕ {suc n} i ≥ Context.m Γ,Δ → Type ℓ ℓ → Context (suc n)
 wkn₁ Γ,Δ i≥m τ = record
   { m≤n = ≤-step m≤n
-- 
cgit v1.2.3