WIP: concrete families

1 files changed, 37 insertions, 0 deletions

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