CHANGELOG

Author: andreasabel

CHANGELOG.md

@@ -1,7 +1,7 @@
 Version 2.1-dev
 ===============
 
-The library has been tested using Agda 2.6.4 and 2.6.4.1.
+The library has been tested using Agda 2.6.4, 2.6.4.1, and 2.6.4.3.
 
 Highlights
 ----------
@@ -33,6 +33,9 @@ Other major improvements
 Deprecated modules
 ------------------
 
+* `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` deprecated in favour of
+  `Data.List.Relation.Binary.Sublist.Propositional.Slice`.
+
 Deprecated names
 ----------------
 
@@ -80,6 +83,12 @@ New modules
   Algebra.Module.Construct.Idealization
   ```
 
+* `Data.List.Relation.Binary.Sublist.Propositional.Slice`
+  replacing `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` (*)
+  and adding new functions:
+  - `⊆-upper-bound-is-cospan` generalising `⊆-disjoint-union-is-cospan` from (*)
+  - `⊆-upper-bound-cospan` generalising `⊆-disjoint-union-cospan` from (*)
+
 * `Data.Vec.Functional.Relation.Binary.Permutation`, defining:
   ```agda
   _↭_ : IRel (Vector A) _
@@ -170,7 +179,7 @@ Additions to existing modules
   quasigroup      : Quasigroup _ _
   isLoop          : IsLoop _∙_ _\\_ _//_ ε
   loop            : Loop _ _
-  
+
   \\-leftDividesˡ  : LeftDividesˡ _∙_ _\\_
   \\-leftDividesʳ  : LeftDividesʳ _∙_ _\\_
   \\-leftDivides   : LeftDivides _∙_ _\\_
@@ -189,7 +198,7 @@ Additions to existing modules
   identityʳ-unique : x ∙ y ≈ x → y ≈ ε
   identity-unique  : Identity x _∙_ → x ≈ ε
   ```
- 
+
 * In `Algebra.Construct.Terminal`:
   ```agda
   rawNearSemiring : RawNearSemiring c ℓ
@@ -218,7 +227,7 @@ Additions to existing modules
   _\\_ : Op₂ A
   x \\ y = (x ⁻¹) ∙ y
   ```
- 
+
 * In `Data.Container.Indexed.Core`:
   ```agda
   Subtrees o c = (r : Response c) → X (next c r)
@@ -301,6 +310,11 @@ Additions to existing modules
   pointwise⊆any : Pointwise R (just x) ⊆ Any (R x)
   ```
 
+* In `Data.List.Relation.Binary.Sublist.Setoid`:
+  ```agda
+  ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ
+  ```
+
 * In `Data.Nat.Divisibility`:
   ```agda
   quotient≢0       : m ∣ n → .{{NonZero n}} → NonZero quotient
@@ -327,7 +341,7 @@ Additions to existing modules
   pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n
   pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n
   ```
-  
+
 * Added new proofs to `Data.Nat.Primality`:
   ```agda
   rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n

standard-library.agda-lib

@@ -1,4 +1,5 @@
-name: standard-library-2.1
+name: standard-library-tbt
 include: src
 flags:
   --warning=noUnsupportedIndexedMatch
+--   --type-based-termination