Setoid version of indexed containers. (#1511)

* Setoid version of indexed containers. Following the structure for non-indexed containers. * An example for indexed containers: multi-sorted algebras. This tests the new setoid version of indexed containers. * Brought code up to date * Added CHANGELOG entry --------- Co-authored-by: MatthewDaggitt <[email protected]>
agda · Mar 16, 2024 · d641582 · d641582
1 parent d0fe603
commit d641582
Show file tree

Hide file tree

Showing 8 changed files with 637 additions and 16 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -75,6 +75,13 @@ New modules
   Relation.Binary.Construct.Interior.Symmetric
   ```
 
+* Pointwise and equality relations over indexed containers:
+  ```agda
+  Data.Container.Indexed.Relation.Binary.Pointwise
+  Data.Container.Indexed.Relation.Binary.Pointwise.Properties
+  Data.Container.Indexed.Relation.Binary.Equality.Setoid
+  ```
+
 Additions to existing modules
 -----------------------------
 
@@ -142,6 +149,11 @@ Additions to existing modules
   idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
   ```
 
+* In `Data.Container.Indexed.Core`:
+  ```agda
+  Subtrees o c = (r : Response c) → X (next c r)
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   nonZeroIndex : Fin n → ℕ.NonZero n

diff --git a/doc/README/Data.agda b/doc/README/Data.agda
@@ -218,7 +218,8 @@ import README.Data.Vec.Relation.Binary.Equality.Cast
 -- monad, least fixed point, etc.) can be used
 
 import README.Data.Container.FreeMonad
-import README.Data.Container.Indexed
+import README.Data.Container.Indexed.VectorExample
+import README.Data.Container.Indexed.MultiSortedAlgebraExample
 
 -- Wrapping n-ary relations into a record definition so type-inference
 -- remembers the things being related.