Wrapping Comments & Fixing Code Delimiters

src/Algebra/Consequences/Setoid.agda

@@ -230,7 +230,7 @@ module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _•_) wh
     (x ⁻¹) • e       ≈⟨ idʳ (x ⁻¹) ⟩
     x ⁻¹             ∎
 
-----------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Bisemigroup-like structures
 
 module _ {_•_ _◦_ : Op₂ A}
@@ -285,7 +285,7 @@ module _ {_•_ _◦_ : Op₂ A}
     (x ◦ (x • z)) • (y ◦ (x • z))  ≈˘⟨ ◦-distribʳ-• _ _ _ ⟩
     (x • y) ◦ (x • z)              ∎
 
-----------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Ring-like structures
 
 module _ {_+_ _*_ : Op₂ A}

src/Algebra/Construct/LexProduct/Inner.agda

@@ -165,8 +165,9 @@ cong₁ a≈b = cong₁₂ a≈b M.refl
 cong₂ : b ≈₁ c → lex a b x y ≈₂ lex a c x y
 cong₂ = cong₁₂ M.refl
 
--- It is possible to relax this. Instead of ∙ being selective and ◦ being associative it's also
--- possible for _◦_ to return a single idempotent element.
+-- It is possible to relax this. Instead of ∙ being selective and ◦
+-- being associative it's also possible for _◦_ to return a single
+-- idempotent element.
 assoc : Associative _≈₁_ _∙_ → Commutative _≈₁_ _∙_ →
         Selective _≈₁_ _∙_ → Associative _≈₂_ _◦_ →
         ∀ a b c x y z  → lex (a ∙ b) c (lex a b x y) z  ≈₂ lex a (b ∙ c) x (lex b c y z)

src/Algebra/Module/Structures.agda

@@ -164,8 +164,9 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr)
   open CommutativeSemiring commutativeSemiring renaming (Carrier to R)
 
   -- An R-semimodule is an R-R-bisemimodule where R is commutative.
-  -- This means that *ₗ and *ᵣ coincide up to mathematical equality, though it
-  -- may be that they do not coincide up to definitional equality.
+  -- This means that *ₗ and *ᵣ coincide up to mathematical equality,
+  -- though it may be that they do not coincide up to definitional
+  -- equality.
 
   record IsSemimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M)
                       : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
@@ -279,8 +280,9 @@ module _ (commutativeRing : CommutativeRing r ℓr)
   open CommutativeRing commutativeRing renaming (Carrier to R)
 
   -- An R-module is an R-R-bimodule where R is commutative.
-  -- This means that *ₗ and *ᵣ coincide up to mathematical equality, though it
-  -- may be that they do not coincide up to definitional equality.
+  -- This means that *ₗ and *ᵣ coincide up to mathematical equality,
+  -- though it may be that they do not coincide up to definitional
+  -- equality.
 
   record IsModule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
     field

src/Algebra/Morphism/Consequences.agda

@@ -15,7 +15,7 @@ open import Function.Base using (id; _∘_)
 open import Function.Definitions
 import Relation.Binary.Reasoning.Setoid as EqR
 
----------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- If f and g are mutually inverse maps between A and B, g is congruent,
 -- f is a homomorphism, then g is a homomorphism.
 

src/Algebra/Properties/CommutativeMagma/Divisibility.agda

@@ -17,12 +17,12 @@ open CommutativeMagma CM
 
 open import Relation.Binary.Reasoning.Setoid setoid
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Re-export the contents of magmas
 
 open import Algebra.Properties.Magma.Divisibility magma public
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Further properties
 
 x∣xy : ∀ x y → x ∣ x ∙ y

src/Algebra/Properties/CommutativeSemigroup.agda

@@ -18,12 +18,12 @@ open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Data.Product.Base using (_,_)
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Re-export the contents of semigroup
 
 open import Algebra.Properties.Semigroup semigroup public
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Properties
 
 interchange : Interchangable _∙_ _∙_
@@ -35,12 +35,12 @@ interchange a b c d = begin
   a ∙ (c ∙ (b ∙ d))  ≈˘⟨ assoc a c (b ∙ d) ⟩
   (a ∙ c) ∙ (b ∙ d)  ∎
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Permutation laws for _∙_ for three factors.
 
 -- There are five nontrivial permutations.
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Partitions (1,1).
 
 x∙yz≈y∙xz :  ∀ x y z → x ∙ (y ∙ z) ≈ y ∙ (x ∙ z)
@@ -72,7 +72,7 @@ x∙yz≈z∙xy x y z = begin
   (x ∙ y) ∙ z   ≈⟨ comm _ z ⟩
   z ∙ (x ∙ y)   ∎
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Partitions (1,2).
 
 -- These permutation laws are proved by composing the proofs for
@@ -93,7 +93,7 @@ x∙yz≈yz∙x x y z =  trans (x∙yz≈y∙zx _ _ _) (sym (assoc y z x))
 x∙yz≈zx∙y :  ∀ x y z → x ∙ (y ∙ z) ≈ (z ∙ x) ∙ y
 x∙yz≈zx∙y x y z =  trans (x∙yz≈z∙xy x y z) (sym (assoc z x y))
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Partitions (2,1).
 
 -- Their laws are proved by composing proofs for partitions (1,1) with
@@ -114,7 +114,7 @@ xy∙z≈y∙zx x y z =  trans (assoc x y z) (x∙yz≈y∙zx x y z)
 xy∙z≈z∙xy :  ∀ x y z → (x ∙ y) ∙ z ≈ z ∙ (x ∙ y)
 xy∙z≈z∙xy x y z =  trans (assoc x y z) (x∙yz≈z∙xy x y z)
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Partitions (2,2).
 
 -- These proofs are by composing with the proofs for (2,1).
@@ -134,13 +134,13 @@ xy∙z≈yz∙x x y z =  trans (xy∙z≈y∙zx x y z) (sym (assoc y z x))
 xy∙z≈zx∙y :  ∀ x y z → (x ∙ y) ∙ z ≈ (z ∙ x) ∙ y
 xy∙z≈zx∙y x y z =  trans (xy∙z≈z∙xy x y z) (sym (assoc z x y))
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- commutative semigroup has Jordan identity
 
 xy∙xx≈x∙yxx : ∀ x y → (x ∙ y) ∙ (x ∙ x) ≈ x ∙ (y ∙ (x ∙ x))
 xy∙xx≈x∙yxx x y = assoc x y ((x ∙ x))
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- commutative semigroup is left/right/middle semiMedial
 
 semimedialˡ : LeftSemimedial _∙_

src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda

@@ -18,18 +18,18 @@ open CommutativeSemigroup CS
 open import Algebra.Properties.CommutativeSemigroup CS using (x∙yz≈xz∙y; x∙yz≈y∙xz)
 open EqReasoning setoid
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Re-export the contents of divisibility over semigroups
 
 open import Algebra.Properties.Semigroup.Divisibility semigroup public
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Re-export the contents of divisibility over commutative magmas
 
 open import Algebra.Properties.CommutativeMagma.Divisibility commutativeMagma public
   using (x∣xy; xy≈z⇒x∣z; ∣-factors; ∣-factors-≈)
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- New properties
 
 x∣y∧z∣x/y⇒xz∣y : ∀ {x y z} → ((x/y , _) : x ∣ y) → z ∣ x/y → x ∙ z ∣ y

src/Algebra/Solver/Ring/NaturalCoefficients.agda

@@ -44,8 +44,8 @@ private
   -- There is a homomorphism from ℕ to R.
   --
   -- Note that the optimised _×_ is used rather than unoptimised _×ᵤ_.
-  -- If _×ᵤ_ were used, then Function.Related.TypeIsomorphisms.test would fail
-  -- to type-check.
+  -- If _×ᵤ_ were used, then Function.Related.TypeIsomorphisms.test
+  -- would fail to type-check.
 
   homomorphism : ℕ-ring -Raw-AlmostCommutative⟶ fromCommutativeSemiring R
   homomorphism = record

src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda

@@ -5,8 +5,8 @@
 -- equality induced by ℕ.
 --
 -- This is sufficient for proving equalities that are independent of the
--- characteristic.  In particular, this is enough for equalities in rings of
--- characteristic 0.
+-- characteristic.  In particular, this is enough for equalities in
+-- rings of characteristic 0.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}

src/Codata/Sized/Delay/Properties.agda

@@ -80,16 +80,16 @@ module _ {a} {A B : Set a} where
   bind̅₂ (later s) {f} (later foo) =
     bind̅₂ (force s) foo
 
-  -- The extracted value of a bind is equivalent to the extracted value of its
-  -- second element
+  -- The extracted value of a bind is equivalent to the extracted value
+  -- of its second element
   extract-bind-⇓ : {d : Delay A Size.∞} → {f : A → Delay B Size.∞} →
                    (d⇓ : d ⇓) → (f⇓ : f (extract d⇓) ⇓) →
                    extract (bind-⇓ d⇓ {f} f⇓) ≡ extract f⇓
   extract-bind-⇓ (now a) f⇓ = Eq.refl
   extract-bind-⇓ (later t) f⇓ = extract-bind-⇓ t f⇓
 
-  -- If the right element of a bind returns a certain value so does the entire
-  -- bind
+  -- If the right element of a bind returns a certain value so does the
+  -- entire bind
   extract-bind̅₂-bind⇓ :
     (d : Delay A ∞) {f : A → Delay B ∞} →
     (bind⇓ : bind d f ⇓) →
@@ -98,8 +98,8 @@ module _ {a} {A B : Set a} where
   extract-bind̅₂-bind⇓ (later s) (later bind⇓) =
     extract-bind̅₂-bind⇓ (force s) bind⇓
 
-  -- Proof that the length of a bind-⇓ is equal to the sum of the length of its
-  -- components.
+  -- Proof that the length of a bind-⇓ is equal to the sum of the length
+  -- of its components.
   bind⇓-length :
       {d : Delay A ∞} {f : A → Delay B ∞} →
       (bind⇓ : bind d f ⇓) →

src/Codata/Sized/M/Bisimilarity.agda

@@ -24,8 +24,8 @@ data Bisim {s p} (C : Container s p) (i : Size) : Rel (M C ∞) (s ⊔ p) where
 
 module _ {s p} {C : Container s p} where
 
-  -- unfortunately the proofs are a lot nicer if we do not use the combinators
-  -- C.refl, C.sym and C.trans
+  -- unfortunately the proofs are a lot nicer if we do not use the
+  -- combinators C.refl, C.sym and C.trans
 
   refl : ∀ {i} → Reflexive (Bisim C i)
   refl {x = inf t} = inf (P.refl , λ where p .force → refl)

src/Codata/Sized/Stream.agda

@@ -127,8 +127,8 @@ chunksOf n = chunksOfAcc n id module ChunksOf where
 interleave : Stream A i → Thunk (Stream A) i → Stream A i
 interleave (x ∷ xs) ys = x ∷ λ where .force → interleave (ys .force) xs
 
--- This interleaving strategy can be generalised to an arbitrary non-empty
--- list of streams
+-- This interleaving strategy can be generalised to an arbitrary
+-- non-empty list of streams
 interleave⁺ : List⁺ (Stream A i) → Stream A i
 interleave⁺ xss =
   List⁺.map head xss
@@ -155,8 +155,8 @@ cantor (l ∷ ls) = zig (l ∷ []) (ls .force) module Cantor where
   zag (x ∷ []) zs (l ∷ ls) = x ∷ λ where .force → zig (l ∷⁺ zs) (ls .force)
   zag (x ∷ (y ∷ xs)) zs ls = x ∷ λ where .force → zag (y ∷ xs) zs ls
 
--- We can use the Cantor zig zag function to define a form of `bind' that
--- reaches any point of the plane in a finite amount of time.
+-- We can use the Cantor zig zag function to define a form of `bind'
+-- that reaches any point of the plane in a finite amount of time.
 plane : {B : A → Set b} → Stream A ∞ → ((a : A) → Stream (B a) ∞) →
         Stream (Σ A B) ∞
 plane as bs = cantor (map (λ a → map (a ,_) (bs a)) as)

src/Data/AVL/Key.agda

@@ -2,7 +2,7 @@
 -- The Agda standard library
 --
 -- This module is DEPRECATED.
------------------------------------------------------------------------
+------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 

src/Data/AVL/Value.agda

@@ -2,7 +2,7 @@
 -- The Agda standard library
 --
 -- This module is DEPRECATED.
------------------------------------------------------------------------
+------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 

src/Data/Empty.agda

@@ -20,10 +20,10 @@ open import Data.Irrelevant using (Irrelevant)
 private
   data Empty : Set where
 
--- ⊥ is defined via Data.Irrelevant (a record with a single irrelevant field)
--- so that Agda can judgementally declare that all proofs of ⊥ are equal
--- to each other. In particular this means that all functions returning a
--- proof of ⊥ are equal.
+-- ⊥ is defined via Data.Irrelevant (a record with a single irrelevant
+-- field) so that Agda can judgementally declare that all proofs of ⊥
+-- are equal to each other. In particular this means that all functions
+-- returning a proof of ⊥ are equal.
 
 ⊥ : Set
 ⊥ = Irrelevant Empty

src/Data/Fin/Permutation/Components.agda

@@ -22,9 +22,9 @@ open import Relation.Binary.PropositionalEquality
 open import Algebra.Definitions using (Involutive)
 open ≡-Reasoning
 
---------------------------------------------------------------------------------
+------------------------------------------------------------------------
 --  Functions
---------------------------------------------------------------------------------
+------------------------------------------------------------------------
 
 -- 'tranpose i j' swaps the places of 'i' and 'j'.
 
@@ -35,9 +35,9 @@ transpose i j k with does (k ≟ i)
 ...   | true  = i
 ...   | false = k
 
---------------------------------------------------------------------------------
+------------------------------------------------------------------------
 --  Properties
---------------------------------------------------------------------------------
+------------------------------------------------------------------------
 
 transpose-inverse : ∀ {n} (i j : Fin n) {k} →
                     transpose i j (transpose j i k) ≡ k

src/Data/Fin/Properties.agda

@@ -818,8 +818,9 @@ punchInᵢ≢i (suc i) (suc j) = punchInᵢ≢i i j ∘ suc-injective
 -- punchOut
 ------------------------------------------------------------------------
 
--- A version of 'cong' for 'punchOut' in which the inequality argument can be
--- changed out arbitrarily (reflecting the proof-irrelevance of that argument).
+-- A version of 'cong' for 'punchOut' in which the inequality argument
+-- can be changed out arbitrarily (reflecting the proof-irrelevance of
+-- that argument).
 
 punchOut-cong : ∀ (i : Fin (suc n)) {j k} {i≢j : i ≢ j} {i≢k : i ≢ k} →
                 j ≡ k → punchOut i≢j ≡ punchOut i≢k
@@ -829,9 +830,9 @@ punchOut-cong {_}     zero    {suc j} {suc k}            = suc-injective
 punchOut-cong {suc n} (suc i) {zero}  {zero}   _ = refl
 punchOut-cong {suc n} (suc i) {suc j} {suc k}    = cong suc ∘ punchOut-cong i ∘ suc-injective
 
--- An alternative to 'punchOut-cong' in the which the new inequality argument is
--- specific. Useful for enabling the omission of that argument during equational
--- reasoning.
+-- An alternative to 'punchOut-cong' in the which the new inequality
+-- argument is specific. Useful for enabling the omission of that
+-- argument during equational reasoning.
 
 punchOut-cong′ : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) →
                  punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym)

src/Data/List/Extrema.agda

@@ -30,7 +30,7 @@ open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; sym; subst) renaming (refl to ≡-refl)
 import Relation.Binary.Construct.On as On
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Setup
 
 open TotalOrder totalOrder renaming (Carrier to B)
@@ -43,7 +43,7 @@ private
     a p : Level
     A : Set a
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Functions
 
 argmin : (A → B) → A → List A → A
@@ -58,7 +58,7 @@ min = argmin id
 max : B → List B → B
 max = argmax id
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Properties of argmin
 
 module _ {f : A → B} where
@@ -114,7 +114,7 @@ argmin-all f {⊤} {xs} {P = P}  p⊤ pxs with argmin-sel f ⊤ xs
 ... | inj₁ argmin≡⊤  = subst P (sym argmin≡⊤) p⊤
 ... | inj₂ argmin∈xs = lookup pxs argmin∈xs
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Properties of argmax
 
 module _ {f : A → B} where
@@ -170,7 +170,7 @@ argmax-all f {P = P} {⊥} {xs} p⊥ pxs with argmax-sel f ⊥ xs
 ... | inj₁ argmax≡⊥  = subst P (sym argmax≡⊥) p⊥
 ... | inj₂ argmax∈xs = lookup pxs argmax∈xs
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Properties of min
 
 min≤v⁺ : ∀ {v} ⊤ xs → ⊤ ≤ v ⊎ Any (_≤ v) xs → min ⊤ xs ≤ v
@@ -208,7 +208,7 @@ min-mono-⊆ : ∀ {⊥₁ ⊥₂ xs ys} → ⊥₁ ≤ ⊥₂ → xs ⊇ ys →
 min-mono-⊆ ⊥₁≤⊥₂ ys⊆xs = min[xs]≤min[ys]⁺ _ _ (inj₁ ⊥₁≤⊥₂)
   (tabulate (inj₂ ∘ Any.map (λ {≡-refl → refl}) ∘ ys⊆xs))
 
-------------------------------------------------------------------------------
+------------------------------------------------------------------------
 -- Properties of max
 
 max≤v⁺ : ∀ {v ⊥ xs} → ⊥ ≤ v → All (_≤ v) xs → max ⊥ xs ≤ v