diff --git a/CHANGELOG.md b/CHANGELOG.md index 186fe9d051..8f6b18bb24 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -170,7 +170,7 @@ Additions to existing modules quasigroup : Quasigroup _ _ isLoop : IsLoop _∙_ _\\_ _//_ ε loop : Loop _ _ - + \\-leftDividesˡ : LeftDividesˡ _∙_ _\\_ \\-leftDividesʳ : LeftDividesʳ _∙_ _\\_ \\-leftDivides : LeftDivides _∙_ _\\_ @@ -189,7 +189,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 +218,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) @@ -327,7 +327,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 diff --git a/CHANGELOG/v2.0.md b/CHANGELOG/v2.0.md index 134309712c..ce3c85e979 100644 --- a/CHANGELOG/v2.0.md +++ b/CHANGELOG/v2.0.md @@ -38,7 +38,7 @@ Bug-fixes Consequently this field has been removed from the record, and the record `IsRingWithoutAnnihilatingZero` in `Algebra.Structures.Biased` has been deprecated as it is now identical to is `IsRing`. - + * In `Algebra.Definitions.RawSemiring` the record `Prime` did not enforce that the number was not divisible by `1#`. To fix this `p∤1 : p ∤ 1#` has been added as a field. @@ -212,7 +212,7 @@ Non-backwards compatible changes * Added new aliases `Is(Meet/Join)(Bounded)Semilattice` for `Is(Bounded)Semilattice` which can be used to indicate meet/join-ness of the original structures, and - the field names in `IsSemilattice` and `Semilattice` have been renamed from + the field names in `IsSemilattice` and `Semilattice` have been renamed from `∧-cong` to `∙-cong`to indicate their undirected nature. * Finally, the following auxiliary files have been moved: @@ -763,10 +763,10 @@ Non-backwards compatible changes - The records in `Function.Structures` and `Function.Bundles` export proofs of these under the names `strictlySurjective`, `strictlyInverseˡ` and `strictlyInverseʳ`, - - Conversion functions for the definitions have been added in both directions - to `Function.Consequences(.Propositional/Setoid)`. - - Conversion functions for structures have been added in - `Function.Structures.Biased`. + - Conversion functions for the definitions have been added in both directions + to `Function.Consequences(.Propositional/Setoid)`. + - Conversion functions for structures have been added in + `Function.Structures.Biased`. ### New `Function.Strict` @@ -852,9 +852,9 @@ Non-backwards compatible changes 4. The modules `Relation.Nullary.(Product/Sum/Implication)` have been deprecated and their contents moved to `Relation.Nullary.(Negation/Reflects/Decidable)`. - + 5. The proof `T?` has been moved from `Data.Bool.Properties` to `Relation.Nullary.Decidable.Core` - (but is still re-exported by the former). + (but is still re-exported by the former). as well as the following breaking changes: @@ -1214,7 +1214,7 @@ Other major improvements * We have then moved raw bundles defined in `Data.X.Properties` to `Data.X.Base` for `X` = `Nat`/`Nat.Binary`/`Integer`/`Rational`/`Rational.Unnormalised`. - + ### Upgrades to `README` sub-library * The `README` sub-library has been moved to `doc/README` and a new `doc/standard-library-doc.agda-lib` has been added. @@ -1223,7 +1223,7 @@ Other major improvements using an out-of-the-box standard Agda installation without altering the main `standard-library.agda-lib` file. -* The second is that the `README` files are now their own first-class library +* The second is that the `README` files are now their own first-class library and can be imported like an other library. Deprecated modules diff --git a/HACKING.md b/HACKING.md index ff859c0507..4e8925648d 100644 --- a/HACKING.md +++ b/HACKING.md @@ -31,7 +31,7 @@ Note on contributions to related/'coupled' modules ================================================== Before making changes to a `Data` module please have a look at related modules -and see if they have any content along similar lines. If so, then please +and see if they have any content along similar lines. If so, then please follow those conventions (e.g. naming, argument order). For example, if working on `Data.Rational`, please check `Data.Rational.Unnormalised` or if working on `Data.Vec` please check `Data.List` and vice versa. diff --git a/fix-whitespace.yaml b/fix-whitespace.yaml index a12022572e..aacf310d54 100644 --- a/fix-whitespace.yaml +++ b/fix-whitespace.yaml @@ -7,5 +7,4 @@ included-files: - "*.md" excluded-files: - - "README/Text/Tabular.agda" - - CHANGELOG.md + - "README/Text/Tabular.agda" \ No newline at end of file diff --git a/src/Algebra/Module/Bundles/Raw.agda b/src/Algebra/Module/Bundles/Raw.agda index b9cc108915..2eb280875f 100644 --- a/src/Algebra/Module/Bundles/Raw.agda +++ b/src/Algebra/Module/Bundles/Raw.agda @@ -200,7 +200,7 @@ record RawBimodule (R : Set r) (S : Set s) m ℓm : Set (r ⊔ s ⊔ suc (m ⊔ ; 0ᴹ = 0ᴹ ; -ᴹ_ = -ᴹ_ } - + rawRightModule : RawRightModule S m ℓm rawRightModule = record { _≈ᴹ_ = _≈ᴹ_ diff --git a/src/Algebra/Morphism/Construct/Initial.agda b/src/Algebra/Morphism/Construct/Initial.agda index 916e181030..883b70109d 100644 --- a/src/Algebra/Morphism/Construct/Initial.agda +++ b/src/Algebra/Morphism/Construct/Initial.agda @@ -39,7 +39,7 @@ zero () -- Basic properties cong : (≈ : Rel A ℓm) → Rel.Homomorphic₂ ℤero.Carrier A ℤero._≈_ ≈ zero -cong _ {x = ()} +cong _ {x = ()} injective : (≈ : Rel A ℓm) → Injective ℤero._≈_ ≈ zero injective _ {x = ()} @@ -52,7 +52,7 @@ isMagmaHomomorphism : (M : RawMagma m ℓm) → isMagmaHomomorphism M = record { isRelHomomorphism = record { cong = cong (RawMagma._≈_ M) } ; homo = λ() - } + } isMagmaMonomorphism : (M : RawMagma m ℓm) → IsMagmaMonomorphism rawMagma M zero diff --git a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda index a8b6464f66..fca4f2793d 100644 --- a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda +++ b/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda @@ -23,7 +23,7 @@ open import Relation.Binary.PropositionalEquality.Core using (refl) open import Relation.Binary.Construct.Composition using (_;_) open Setoid S renaming (Carrier to A) -open import Relation.Binary.Properties.Setoid S using (≈;≈⇒≈; ≈⇒≈;≈) +open import Relation.Binary.Properties.Setoid S using (≈;≈⇒≈; ≈⇒≈;≈) open import Data.List.Relation.Ternary.Appending.Setoid S private diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index fed89d7d45..6dda6bac9d 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -34,7 +34,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans private variable n : ℕ - + ------------------------------------------------------------------------ -- Core definition @@ -107,18 +107,18 @@ factorise n₀@(2+ _) = build [ <-recBuilder ⊗ <-recBuilder ] P facRec (n₀ , pred (m * m) <⟨ s1⇒nonTrivial (quotient>1 m∣n m