From 25feb8c72e5e4a76fbd4ab381105de6c19d6ab50 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 19 Feb 2025 15:47:36 +0000
Subject: Update to stdlib 2.1.1 and other changes.

I don't fully know what has changed because the changes are so old.

Doesn't yet compile due to not finishing proofs in `CBPV.Frex.Comp`.
---
 src/CBPV/Context.agda | 35 +++++++++++++++++++++++++++--------
 1 file changed, 27 insertions(+), 8 deletions(-)

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

diff --git a/src/CBPV/Context.agda b/src/CBPV/Context.agda
index d1aafc4..0ab5093 100644
--- a/src/CBPV/Context.agda
+++ b/src/CBPV/Context.agda
@@ -1,6 +1,7 @@
 module CBPV.Context where
 
 open import Data.Bool using (Bool)
+open import Data.List using (List; []; _∷_)
 open import Data.String using (String)
 import Data.String.Properties as String
 
@@ -15,23 +16,41 @@ abstract
   𝔪 : Name
   𝔪 = "𝔪"
 
-record Named : Set where
+record GenNamed (A : Set) : Set where
   constructor _:-_
   field
     name   : Name
-    ofType : ValType
+    ofType : A
 
-open Named public
+open GenNamed public
 
-infixl 5 _:<_ _++_
+Named : Set
+Named = GenNamed ValType
 
-data Context : Set where
-  [<]  : Context
-  _:<_ : Context → (ex : Named) → Context
+infixl 5 _:<_ _++_ _<><_
+
+data GenContext (A : Set) : Set where
+  [<]  : GenContext A
+  _:<_ : GenContext A → (ex : GenNamed A) → GenContext A
+
+Context : Set
+Context = GenContext ValType
+
+map : {A B : Set} → (A → B) → GenContext A → GenContext B
+map f [<] = [<]
+map f (Γ :< (n :- ty)) = map f Γ :< (n :- f ty)
+
+foldr : {A B : Set} → (A → B → B) → B → GenContext A → B
+foldr f z [<] = z
+foldr f z (Γ :< ex) = foldr f (f (ex .ofType) z) Γ
 
 pattern [<_:-_] x A = [<] :< (x :- A)
 pattern [<_:-_,_:-_] x A y A′ = [<] :< (x :- A) :< (y :- A′)
 
-_++_ : Context → Context → Context
+_++_ : {A : Set} → GenContext A → GenContext A → GenContext A
 Γ ++ [<] = Γ
 Γ ++ (Δ :< ex) = Γ ++ Δ :< ex
+
+_<><_ : {A : Set} → GenContext A → List (GenNamed A) → GenContext A
+Γ <>< [] = Γ
+Γ <>< (x ∷ xs) = Γ :< x <>< xs
-- 
cgit v1.2.3