From adad5280af0d81a2f171df619e9c7169dcb43a02 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 27 Mar 2021 20:32:03 +0000
Subject: Introduce non-terminating proof of derivation existence.

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

(limited to 'src/Cfe/Context/Base.agda')

diff --git a/src/Cfe/Context/Base.agda b/src/Cfe/Context/Base.agda
index 2814a64..a428d3c 100644
--- a/src/Cfe/Context/Base.agda
+++ b/src/Cfe/Context/Base.agda
@@ -54,6 +54,8 @@ record Context n : Set (c ⊔ lsuc ℓ) where
     Γ : Vec (Type ℓ ℓ) (n ∸ m)
     Δ : Vec (Type ℓ ℓ) m
 
+∙,∙ : Context 0
+∙,∙ = record { m≤n = z≤n ; Γ = [] ; Δ = [] }
 
 toVec : ∀ {n} → Context n → Vec (Type ℓ ℓ) n
 toVec record { m = .0 ; m≤n = _ ; Γ = Γ ; Δ = [] } = Γ
-- 
cgit v1.2.3