Skip to content

Commit

Permalink
[ fix ] tidy up alphabetical ordering in CHANGELOG (#2538)
Browse files Browse the repository at this point in the history 
* tidy up alphabetical ordering

* refactor: more comprehensive overhaul
  • Loading branch information
@jamesmckinna
jamesmckinna authored Jan 2, 2025
1 parent d481f5c commit 11d0a33
Showing 1 changed file with 87 additions and 92 deletions.
179 changes: 87 additions & 92 deletions CHANGELOG.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,18 +9,17 @@ Highlights
Bug-fixes
---------

* Removed unnecessary parameter `#-trans : Transitive _#_` from
`Relation.Binary.Reasoning.Base.Apartness`.
* Relax the types for `≡-syntax` in `Relation.Binary.HeterogeneousEquality`.
These operators are used for equational reasoning of heterogeneous equality
`x ≅ y`, but previously the three operators in `≡-syntax` unnecessarily require
`x` and `y` to have the same type, making them unusable in most situations.

* Removed unnecessary parameter `#-trans : Transitive _#_` from
`Relation.Binary.Reasoning.Base.Apartness`.

Non-backwards compatible changes
--------------------------------

* In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold.

* In `Data.List.Relation.Binary.Sublist.Propositional.Properties` the implicit module parameters `a` and `A` have been replaced with `variable`s. This should be a backwards compatible change for the overwhelming majority of uses, and would only be non-backwards compatible if you were explicitly supplying these implicit parameters for some reason when importing the module. Explicitly supplying the implicit parameters for functions exported from the module should not be affected.

* The names exposed by the `IsSemiringWithoutOne` record have been altered to
Expand All @@ -32,6 +31,8 @@ Non-backwards compatible changes

* [issue #2504](https://github.com/agda/agda-stdlib/issues/2504) and [issue #2519](https://github.com/agda/agda-stdlib/issues/2510) In `Data.Nat.Base` the definitions of `_≤′_` and `_≤‴_` have been modified to make the witness to equality explicit in new constructors `≤′-reflexive` and `≤‴-reflexive`; pattern synonyms `≤′-refl` and `≤‴-refl` have been added for backwards compatibility but NB. the change in parametrisation means that these patterns are *not* necessarily well-formed if the old implicit arguments `m`,`n` are supplied explicitly.

* In `Function.Related.TypeIsomorphisms`, the unprimed versions are more level polymorphic; and the primed versions retain `Level` homogeneous types for the `Semiring` axioms to hold.

Minor improvements
------------------

Expand Down Expand Up @@ -109,16 +110,6 @@ Deprecated names
New modules
-----------

* Bundled morphisms between (raw) algebraic structures:
```
Algebra.Morphism.Bundles
```

* Properties of `IdempotentCommutativeMonoid`s refactored out from `Algebra.Solver.IdempotentCommutativeMonoid`:
```agda
Algebra.Properties.IdempotentCommutativeMonoid
```

* Consequences of module monomorphisms
```agda
Algebra.Module.Morphism.BimoduleMonomorphism
Expand All @@ -131,6 +122,16 @@ New modules
Algebra.Module.Morphism.SemimoduleMonomorphism
```

* Bundled morphisms between (raw) algebraic structures:
```
Algebra.Morphism.Bundles
```

* Properties of `IdempotentCommutativeMonoid`s refactored out from `Algebra.Solver.IdempotentCommutativeMonoid`:
```agda
Algebra.Properties.IdempotentCommutativeMonoid
```

* Refactoring of the `Algebra.Solver.*Monoid` implementations, via
a single `Solver` module API based on the existing `Expr`, and
a common `Normal`-form API:
Expand All @@ -144,37 +145,37 @@ New modules

NB Imports of the existing proof procedures `solve` and `prove` etc. should still be via the top-level interfaces in `Algebra.Solver.*Monoid`.

* Refactored out from `Data.List.Relation.Unary.All.Properties` in order to break a dependency cycle with `Data.List.Membership.Setoid.Properties`:
```agda
Data.List.Relation.Unary.All.Properties.Core
```
* `Data.List.Effectful.Foldable`: `List` is `Foldable`

* `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
Propositional counterpart to `Data.List.Relation.Binary.Disjoint.Setoid.Properties`
```agda
sum-↭ : sum Preserves _↭_ ⟶ _≡_
```

* `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`
* Added `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`

* Refactored out from `Data.List.Relation.Unary.All.Properties` in order to break a dependency cycle with `Data.List.Membership.Setoid.Properties`:
```agda
Data.List.Relation.Unary.All.Properties.Core
```

* Refactored `Data.Refinement` into:
```agda
Data.Refinement.Base
Data.Refinement.Properties
```

* `Data.Vec.Effectful.Foldable`: `Vec` is `Foldable`

* `Effect.Foldable`: implementation of haskell-like `Foldable`

* Raw bundles for the `Relation.Binary.Bundles` hierarchy:
```agda
Relation.Binary.Bundles.Raw
```
plus adding `rawX` fields to each of `Relation.Binary.Bundles.X`.

* `Data.List.Effectful.Foldable`: `List` is `Foldable`

* `Data.Vec.Effectful.Foldable`: `Vec` is `Foldable`

* `Effect.Foldable`: implementation of haskell-like `Foldable`

Additions to existing modules
-----------------------------

Expand Down Expand Up @@ -292,22 +293,6 @@ Additions to existing modules
isNearSemiring : IsNearSemiring _ _
```

* In `Data.List.Membership.Setoid.Properties`:
```agda
∉⇒All[≉] : x ∉ xs → All (x ≉_) xs
All[≉]⇒∉ : All (x ≉_) xs → x ∉ xs
Any-∈-swap : Any (_∈ ys) xs → Any (_∈ xs) ys
All-∉-swap : All (_∉ ys) xs → All (_∉ xs) ys
∈-map∘filter⁻ : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x
∈-map∘filter⁺ : f Preserves _≈₁_ ⟶ _≈₂_ →
∃[ x ] x ∈₁ xs × y ≈₂ f x × P x →
y ∈₂ map f (filter P? xs)
∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
∉[] : x ∉ []
deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs
```

* In `Data.List.Membership.Propositional.Properties`:
```agda
∈-AllPairs₂ : AllPairs R xs → x ∈ xs → y ∈ xs → x ≡ y ⊎ R x y ⊎ R y x
Expand All @@ -329,6 +314,22 @@ Additions to existing modules
unique∧set⇒bag : Unique xs → Unique ys → xs ∼[ set ] ys → xs ∼[ bag ] ys
```

* In `Data.List.Membership.Setoid.Properties`:
```agda
∉⇒All[≉] : x ∉ xs → All (x ≉_) xs
All[≉]⇒∉ : All (x ≉_) xs → x ∉ xs
Any-∈-swap : Any (_∈ ys) xs → Any (_∈ xs) ys
All-∉-swap : All (_∉ ys) xs → All (_∉ xs) ys
∈-map∘filter⁻ : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x
∈-map∘filter⁺ : f Preserves _≈₁_ ⟶ _≈₂_ →
∃[ x ] x ∈₁ xs × y ≈₂ f x × P x →
y ∈₂ map f (filter P? xs)
∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
∉[] : x ∉ []
deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs
```

* In `Data.List.Properties`:
```agda
product≢0 : All NonZero ns → NonZero (product ns)
Expand All @@ -342,37 +343,14 @@ Additions to existing modules
([] , [])
```

* In `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
```agda
⊆⇒⊆ₛ : (S : Setoid a ℓ) → as ⊆ bs → as (SetoidSublist.⊆ S) bs
```

* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
```agda
concat⁺ : Sublist _⊆_ ass bss → concat ass ⊆ concat bss
all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
```

* In `Data.List.Relation.Unary.All.Properties`:
```agda
all⇒dropWhile≡[] : (P? : Decidable P) → All P xs → dropWhile P? xs ≡ []
all⇒takeWhile≗id : (P? : Decidable P) → All P xs → takeWhile P? xs ≡ xs
```

* In `Data.List.Relation.Unary.Any.Properties`:
```agda
concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs)
concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs
```

* In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
```agda
Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
```

* In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`:
```agda
Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
```

* In `Data.List.Relation.Binary.Equality.Setoid`:
Expand Down Expand Up @@ -410,6 +388,12 @@ Additions to existing modules
product-↭ : product Preserves _↭_ ⟶ _≡_
```

* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
```agda
dedup-++-↭ : Disjoint xs ys →
deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys
```

* In `Data.List.Relation.Binary.Permutation.Setoid`:
```agda
↭-reflexive-≋ : _≋_ ⇒ _↭_
Expand All @@ -431,60 +415,71 @@ Additions to existing modules
++⁺ʳ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
```

* In `Data.List.Relation.Unary.All`:
* In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
```agda
search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
```
Sublist-[]-universal : Universal (Sublist R [])
```

* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
* In `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
```agda
∷⊈[] : x ∷ xs ⊈ []
⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
⊆⇒⊆ₛ : (S : Setoid a ℓ) → as ⊆ bs → as (SetoidSublist.⊆ S) bs
```

* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
```agda
[]⊆-universal : Universal ([] ⊆_)
concat⁺ : Sublist _⊆_ ass bss → concat ass ⊆ concat bss
all⊆concat : (xss : List (List A)) → All (Sublist._⊆ concat xss) xss
```

* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
```agda
∷⊈[] : x ∷ xs ⊈ []
⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
```

* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
```agda
concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
∷⊈[] : x ∷ xs ⊈ []
⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
```

* In `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
* In `Data.List.Relation.Unary.First.Properties`:
```agda
Sublist-[]-universal : Universal (Sublist R [])
¬First⇒All : ∁ Q ⊆ P → ∁ (First P Q) ⊆ All P
¬All⇒First : Decidable P → ∁ P ⊆ Q → ∁ (All P) ⊆ First P Q
```

* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
* In `Data.List.Relation.Unary.All`:
```agda
[]⊆-universal : Universal ([] ⊆_)
search : Decidable P → ∀ xs → All (∁ P) xs ⊎ Any P xs
```

* In `Data.List.Relation.Binary.Disjoint.Setoid.Properties`:
* In `Data.List.Relation.Unary.All.Properties`:
```agda
deduplicate⁺ : Disjoint S xs ys → Disjoint S (deduplicate _≟_ xs) (deduplicate _≟_ ys)
all⇒dropWhile≡[] : (P? : Decidable P) → All P xs → dropWhile P? xs ≡ []
all⇒takeWhile≗id : (P? : Decidable P) → All P xs → takeWhile P? xs ≡ xs
```

* In `Data.List.Relation.Binary.Disjoint.Propositional.Properties`:
* In `Data.List.Relation.Unary.Any.Properties`:
```agda
deduplicate⁺ : Disjoint xs ys → Disjoint (deduplicate _≟_ xs) (deduplicate _≟_ ys)
concatMap⁺ : Any (Any P ∘ f) xs → Any P (concatMap f xs)
concatMap⁻ : Any P (concatMap f xs) → Any (Any P ∘ f) xs
```

* In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
* In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
```agda
dedup-++-↭ : Disjoint xs ys →
deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys
Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
```

* In `Data.List.Relation.Unary.First.Properties`:
* In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
```agda
¬First⇒All : ∁ Q ⊆ P → ∁ (First P Q) ⊆ All P
¬All⇒First : Decidable P → ∁ P ⊆ Q → ∁ (All P) ⊆ First P Q
Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
```

* In `Data.Maybe.Properties`:
Expand All @@ -503,7 +498,7 @@ Additions to existing modules
≥‴-irrelevant : Irrelevant {A = ℕ} _≥‴_
```

adjunction between `suc` and `pred`
Added adjunction between `suc` and `pred`
```agda
suc[m]≤n⇒m≤pred[n] : suc m ≤ n → m ≤ pred n
m≤pred[n]⇒suc[m]≤n : .{{NonZero n}} → m ≤ pred n → suc m ≤ n
Expand Down

0 comments on commit 11d0a33

Please sign in to comment.