From 7e0169f7b6b9cb4c4323c320982c93e622999943 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Mon, 26 Feb 2024 13:19:53 +0000
Subject: WIP: concrete families

---
 src/CBPV/Context.agda | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 src/CBPV/Context.agda

(limited to 'src/CBPV/Context.agda')

diff --git a/src/CBPV/Context.agda b/src/CBPV/Context.agda
new file mode 100644
index 0000000..d1aafc4
--- /dev/null
+++ b/src/CBPV/Context.agda
@@ -0,0 +1,37 @@
+module CBPV.Context where
+
+open import Data.Bool using (Bool)
+open import Data.String using (String)
+import Data.String.Properties as String
+
+open import Relation.Binary.Definitions using (DecidableEquality)
+
+open import CBPV.Type
+
+abstract
+  Name : Set
+  Name = String
+
+  𝔪 : Name
+  𝔪 = "𝔪"
+
+record Named : Set where
+  constructor _:-_
+  field
+    name   : Name
+    ofType : ValType
+
+open Named public
+
+infixl 5 _:<_ _++_
+
+data Context : Set where
+  [<]  : Context
+  _:<_ : Context → (ex : Named) → Context
+
+pattern [<_:-_] x A = [<] :< (x :- A)
+pattern [<_:-_,_:-_] x A y A′ = [<] :< (x :- A) :< (y :- A′)
+
+_++_ : Context → Context → Context
+Γ ++ [<] = Γ
+Γ ++ (Δ :< ex) = Γ ++ Δ :< ex
-- 
cgit v1.2.3