From 31f31262de61e08d753302dd9c14ea1b1d0eca8b Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 16 Oct 2023 19:15:50 +0100
Subject: [PATCH 1/3] fixed typos
---
src/Function/Bundles.agda | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index a51dc4ea84..700b673857 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -182,7 +182,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
open Func toFunction public
using (module Eq₁; module Eq₂)
- renaming (isCongruent to to-isCongrunet)
+ renaming (isCongruent to to-isCongruent)
fromFunction : Func To From
fromFunction = record
@@ -192,7 +192,7 @@ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
open Func fromFunction public
using ()
- renaming (isCongruent to from-isCongrunet)
+ renaming (isCongruent to from-isCongruent)
record LeftInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
From 58afa7094c0f57e5093d0c86be01f87ea93a5e22 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 16 Oct 2023 19:17:51 +0100
Subject: [PATCH 2/3] fixed alignment typo caught in #2054
---
CHANGELOG.md | 58 ++++++++++++++++++++++++++--------------------------
1 file changed, 29 insertions(+), 29 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index a1fb08efcf..b7369380f5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -539,7 +539,7 @@ Non-backwards compatible changes
3. Finally, if the above approaches are not viable then you may be forced to explicitly
use `cong` combined with a lemma that proves the old reduction behaviour.
-* Similarly, in order to prevent reduction, the equality `_≃_` in `Data.Rational.Base`
+* Similarly, in order to prevent reduction, the equality `_≃_` in `Data.Rational.Base`
has been made into a data type with the single constructor `*≡*`. The destructor `drop-*≡*`
has been added to `Data.Rational.Properties`.
@@ -606,7 +606,7 @@ Non-backwards compatible changes
with the consequence that all arguments involving about accesibility and
wellfoundedness proofs were polluted by almost-always-inferrable explicit
arguments for the `y` position. The definition has now been changed to
- make that argument *implicit*, as
+ make that argument *implicit*, as
```agda
WfRec : Rel A r → ∀ {ℓ} → RecStruct A ℓ _
WfRec _<_ P x = ∀ {y} → y < x → P y
@@ -931,40 +931,40 @@ Non-backwards compatible changes
as would be expected. Instead it omitted several fields like irreflexivity as they were derivable from the
proof of trichotomy. However, this led to problems further up the hierarchy where bundles such as `StrictTotalOrder`
which contained multiple distinct proofs of `IsStrictPartialOrder`.
-
-* To remedy this the definition of `IsStrictTotalOrder` has been changed to so that it builds upon
- `IsStrictPartialOrder` as would be expected.
+
+* To remedy this the definition of `IsStrictTotalOrder` has been changed to so that it builds upon
+ `IsStrictPartialOrder` as would be expected.
* To aid migration, the old record definition has been moved to `Relation.Binary.Structures.Biased`
- which contains the `isStrictTotalOrderᶜ` smart constructor (which is re-exported by `Relation.Binary`) .
+ which contains the `isStrictTotalOrderᶜ` smart constructor (which is re-exported by `Relation.Binary`) .
Therefore the old code:
```agda
<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = record
- { isEquivalence = isEquivalence
- ; trans = <-trans
- ; compare = <-cmp
- }
+ { isEquivalence = isEquivalence
+ ; trans = <-trans
+ ; compare = <-cmp
+ }
```
can be migrated either by updating to the new record fields if you have a proof of `IsStrictPartialOrder`
available:
```agda
<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = record
- { isStrictPartialOrder = <-isStrictPartialOrder
- ; compare = <-cmp
- }
+ { isStrictPartialOrder = <-isStrictPartialOrder
+ ; compare = <-cmp
+ }
```
or simply applying the smart constructor to the record definition as follows:
```agda
<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = isStrictTotalOrderᶜ record
- { isEquivalence = isEquivalence
- ; trans = <-trans
- ; compare = <-cmp
- }
+ { isEquivalence = isEquivalence
+ ; trans = <-trans
+ ; compare = <-cmp
+ }
```
-
+
### Changes to triple reasoning interface
* The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict
@@ -987,7 +987,7 @@ Non-backwards compatible changes
Data.Vec.Relation.Binary.Lex.NonStrict
Relation.Binary.Reasoning.StrictPartialOrder
Relation.Binary.Reasoning.PartialOrder
- ```
+ ```
### Other
@@ -1165,7 +1165,7 @@ Non-backwards compatible changes
* `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to
`¬¬-excluded-middle`.
-* `iterate` and `replicate` in `Data.Vec.Base` and `Data.Vec.Functional`
+* `iterate` and `replicate` in `Data.Vec.Base` and `Data.Vec.Functional`
now take the length of vector, `n`, as an explicit rather than an implicit argument.
```agda
iterate : (A → A) → A → ∀ n → Vec A n
@@ -1231,11 +1231,11 @@ Major improvements
### More modular design of equational reasoning.
-* Have introduced a new module `Relation.Binary.Reasoning.Syntax` which exports
+* Have introduced a new module `Relation.Binary.Reasoning.Syntax` which exports
a range of modules containing pre-existing reasoning combinator syntax.
-* This makes it possible to add new or rename existing reasoning combinators to a
- pre-existing `Reasoning` module in just a couple of lines
+* This makes it possible to add new or rename existing reasoning combinators to a
+ pre-existing `Reasoning` module in just a couple of lines
(e.g. see `∣-Reasoning` in `Data.Nat.Divisibility`)
Deprecated modules
@@ -1813,7 +1813,7 @@ Deprecated names
```agda
_↔⟨⟩_ ↦ _≡⟨⟩_
```
-
+
* In `Foreign.Haskell.Either` and `Foreign.Haskell.Pair`:
```
toForeign ↦ Foreign.Haskell.Coerce.coerce
@@ -2706,7 +2706,7 @@ Additions to existing modules
toℕ-inverseˡ : Inverseˡ _≡_ _≡_ toℕ fromℕ
toℕ-inverseʳ : Inverseʳ _≡_ _≡_ toℕ fromℕ
toℕ-inverseᵇ : Inverseᵇ _≡_ _≡_ toℕ fromℕ
-
+
<-asym : Asymmetric _<_
```
@@ -3163,7 +3163,7 @@ Additions to existing modules
∀ {m n} → _Respectsʳ_ (_<_ {m} {n}) _≋_
<-wellFounded : Transitive _≈_ → _≺_ Respectsʳ _≈_ → WellFounded _≺_ →
∀ {n} → WellFounded (_<_ {n})
-```
+ ```
* Added new functions in `Data.Vec.Relation.Unary.Any`:
```
@@ -3190,9 +3190,9 @@ Additions to existing modules
* Added new application operator synonym to `Function.Bundles`:
```agda
_⟨$⟩_ : Func From To → Carrier From → Carrier To
- _⟨$⟩_ = Func.to
+ _⟨$⟩_ = Func.to
```
-
+
* Added new proofs in `Function.Construct.Symmetry`:
```
bijective : Bijective ≈₁ ≈₂ f → Symmetric ≈₂ → Transitive ≈₂ → Congruent ≈₁ ≈₂ f → Bijective ≈₂ ≈₁ f⁻¹
@@ -3888,7 +3888,7 @@ This is a full list of proofs that have changed form to use irrelevant instance
blockerAll : List Blocker → Blocker
blockTC : Blocker → TC A
```
-
+
* Added new file `Relation.Binary.Reasoning.Base.Apartness`
This is how to use it:
From a9a356aa684b54e6387193d49a3be4af601aebaa Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 16 Oct 2023 19:18:14 +0100
Subject: [PATCH 3/3] `fix-whitespace`
---
src/Function/Bundles.agda | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
index 700b673857..0aef27fc57 100644
--- a/src/Function/Bundles.agda
+++ b/src/Function/Bundles.agda
@@ -481,7 +481,7 @@ module _ {A : Set a} {B : Set b} where
module _ {From : Setoid a ℓ₁} {To : Setoid b ℓ₂} where
open Setoid
-
+
infixl 5 _⟨$⟩_
_⟨$⟩_ : Func From To → Carrier From → Carrier To
_⟨$⟩_ = Func.to