diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index 07b75806c2..e32d4969a1 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/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} diff --git a/src/Algebra/Construct/LexProduct/Inner.agda b/src/Algebra/Construct/LexProduct/Inner.agda index d235c1b8fd..9b6e06f0e6 100644 --- a/src/Algebra/Construct/LexProduct/Inner.agda +++ b/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) diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index 4a0e40c17c..9fe1f85191 100644 --- a/src/Algebra/Module/Structures.agda +++ b/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 diff --git a/src/Algebra/Morphism/Consequences.agda b/src/Algebra/Morphism/Consequences.agda index ac7d6de2c5..c81e55a7bb 100644 --- a/src/Algebra/Morphism/Consequences.agda +++ b/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. diff --git a/src/Algebra/Properties/CommutativeMagma/Divisibility.agda b/src/Algebra/Properties/CommutativeMagma/Divisibility.agda index 27f6ba56a5..3f6cae0f0c 100644 --- a/src/Algebra/Properties/CommutativeMagma/Divisibility.agda +++ b/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 diff --git a/src/Algebra/Properties/CommutativeSemigroup.agda b/src/Algebra/Properties/CommutativeSemigroup.agda index e09253ece7..0c27a5e96b 100644 --- a/src/Algebra/Properties/CommutativeSemigroup.agda +++ b/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 _∙_ diff --git a/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda b/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda index 66bec51115..da8d3abf45 100644 --- a/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda +++ b/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 diff --git a/src/Algebra/Solver/Ring/NaturalCoefficients.agda b/src/Algebra/Solver/Ring/NaturalCoefficients.agda index fdd0a65e6b..6d3ab81b37 100644 --- a/src/Algebra/Solver/Ring/NaturalCoefficients.agda +++ b/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 diff --git a/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda b/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda index 84003922a0..9b9671c527 100644 --- a/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda +++ b/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 #-} diff --git a/src/Codata/Sized/Delay/Properties.agda b/src/Codata/Sized/Delay/Properties.agda index e491178c71..39a56d1ef9 100644 --- a/src/Codata/Sized/Delay/Properties.agda +++ b/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 ⇓) → diff --git a/src/Codata/Sized/M/Bisimilarity.agda b/src/Codata/Sized/M/Bisimilarity.agda index 3a60a91d16..69bb8244a3 100644 --- a/src/Codata/Sized/M/Bisimilarity.agda +++ b/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) diff --git a/src/Codata/Sized/Stream.agda b/src/Codata/Sized/Stream.agda index 4b7d6bd37d..34a9583448 100644 --- a/src/Codata/Sized/Stream.agda +++ b/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) diff --git a/src/Data/AVL/Key.agda b/src/Data/AVL/Key.agda index 30eaf2f5aa..96023d342d 100644 --- a/src/Data/AVL/Key.agda +++ b/src/Data/AVL/Key.agda @@ -2,7 +2,7 @@ -- The Agda standard library -- -- This module is DEPRECATED. ------------------------------------------------------------------------ +------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} diff --git a/src/Data/AVL/Value.agda b/src/Data/AVL/Value.agda index 4ddbc30003..d46bde80eb 100644 --- a/src/Data/AVL/Value.agda +++ b/src/Data/AVL/Value.agda @@ -2,7 +2,7 @@ -- The Agda standard library -- -- This module is DEPRECATED. ------------------------------------------------------------------------ +------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} diff --git a/src/Data/Empty.agda b/src/Data/Empty.agda index ff98565038..990a9a1632 100644 --- a/src/Data/Empty.agda +++ b/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 diff --git a/src/Data/Fin/Permutation/Components.agda b/src/Data/Fin/Permutation/Components.agda index b053cee86b..2db835719c 100644 --- a/src/Data/Fin/Permutation/Components.agda +++ b/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 diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda index e181a291e9..615728e971 100644 --- a/src/Data/Fin/Properties.agda +++ b/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) diff --git a/src/Data/List/Extrema.agda b/src/Data/List/Extrema.agda index 8d71aab6a7..5abc5edee9 100644 --- a/src/Data/List/Extrema.agda +++ b/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 diff --git a/src/Data/List/Fresh.agda b/src/Data/List/Fresh.agda index 72c372003a..b5a5718765 100644 --- a/src/Data/List/Fresh.agda +++ b/src/Data/List/Fresh.agda @@ -1,9 +1,9 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Fresh lists, a proof relevant variant of Catarina Coquand's contexts in --- "A Formalised Proof of the Soundness and Completeness of a Simply Typed --- Lambda-Calculus with Explicit Substitutions" +-- Fresh lists, a proof relevant variant of Catarina Coquand's contexts +-- in "A Formalised Proof of the Soundness and Completeness of a Simply +-- Typed Lambda-Calculus with Explicit Substitutions" ------------------------------------------------------------------------ -- See README.Data.List.Fresh and README.Data.Trie.NonDependent for @@ -52,8 +52,8 @@ module _ {a} (A : Set a) (R : Rel A r) where -- the erasure ⌊_⌋ of a decidable predicate, cf. Relation.Nary) or we -- do not care about the proof, it is convenient to get back list syntax. - -- We use a different symbol to avoid conflict when importing both Data.List - -- and Data.List.Fresh. + -- We use a different symbol to avoid conflict when importing both + -- Data.List and Data.List.Fresh. infixr 5 _∷#_ pattern _∷#_ x xs = cons x xs _ diff --git a/src/Data/List/Kleene/AsList.agda b/src/Data/List/Kleene/AsList.agda index bb2c52b603..0b6d4c033d 100644 --- a/src/Data/List/Kleene/AsList.agda +++ b/src/Data/List/Kleene/AsList.agda @@ -54,9 +54,9 @@ infixr 5 _∷_ pattern _∷_ x xs = Kleene.∹ x Kleene.& xs ------------------------------------------------------------------------ --- The following functions change the type of the list (from ⁺ to * or vice --- versa) in Data.KleeneList, so we reimplement them here to keep the --- type the same. +-- The following functions change the type of the list (from ⁺ to * or +-- vice versa) in Data.KleeneList, so we reimplement them here to keep +-- the type the same. scanr : (A → B → B) → B → List A → List B scanr f b xs = Kleene.∹ Kleene.scanr* f b xs diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index c4cf722ec6..254bf336f9 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -54,7 +54,7 @@ private D : Set d E : Set e ------------------------------------------------------------------------ +------------------------------------------------------------------------ -- _∷_ module _ {x y : A} {xs ys : List A} where @@ -770,7 +770,8 @@ take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i) = take-suc (tabulate f) (cast _ i) --- If you take at least as many elements from a list as it has, you get the whole list. +-- If you take at least as many elements from a list as it has, you get +-- the whole list. take-all :(n : ℕ) (xs : List A) → n ≥ length xs → take n xs ≡ xs take-all zero [] _ = refl take-all (suc _) [] _ = refl diff --git a/src/Data/List/Relation/Binary/Lex/Core.agda b/src/Data/List/Relation/Binary/Lex/Core.agda index 96549e013b..0b3e821194 100644 --- a/src/Data/List/Relation/Binary/Lex/Core.agda +++ b/src/Data/List/Relation/Binary/Lex/Core.agda @@ -35,7 +35,7 @@ data Lex {A : Set a} (P : Set) next : ∀ {x xs y ys} (x≈y : x ≈ y) (xs0 {1+[2 _ ]} _ = 0 _ _ y0 : x < y → y ∸ x > 0ᵇ x0 {x} {y} = toℕ-cancel-< ∘ subst (ℕ._> 0) (sym (toℕ-homo-∸ y x)) ∘ ℕₚ.m x) ≈ x fmapIdₗ x = A.refl , refl open RawMonad monad - -- Now, let's show that "pure" is a unit for >>=. We use Lift in exactly - -- the same way as above. The data (x : B) then needs to be "lifted" to - -- this new type (Lift B). + -- Now, let's show that "pure" is a unit for >>=. We use Lift in + -- exactly the same way as above. The data (x : B) then needs to be + -- "lifted" to this new type (Lift B). pureUnitL : ∀ {x : B} {f : Lift a B → A.Carrier × Lift a B} → (pure (lift x) >>= f) ≈ f (lift x) pureUnitL = A.identityˡ _ , refl diff --git a/src/Data/Product/Nary/NonDependent.agda b/src/Data/Product/Nary/NonDependent.agda index cb421f16b6..29bb483964 100644 --- a/src/Data/Product/Nary/NonDependent.agda +++ b/src/Data/Product/Nary/NonDependent.agda @@ -28,13 +28,14 @@ open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong open import Function.Nary.NonDependent.Base --- Provided n Levels and a corresponding "vector" of `n` Sets, we can build a big --- right-nested product type packing a value for each one of these Sets. +-- Provided n Levels and a corresponding "vector" of `n` Sets, we can +-- build a big right-nested product type packing a value for each one +-- of these Sets. -- We have two distinct but equivalent definitions: -- the first which is always ⊤-terminated --- the other which has a special case for n = 1 because we want our `(un)curryₙ` --- functions to work for user-written functions and products and they rarely are --- ⊤-terminated. +-- the other which has a special case for n = 1 because we want our +-- `(un)curryₙ` functions to work for user-written functions and +-- products and they rarely are ⊤-terminated. Product⊤ : ∀ n {ls} → Sets n ls → Set (⨆ n ls) Product⊤ zero as = ⊤ @@ -143,8 +144,8 @@ fromEqualₙ (suc n@(suc _)) eq = uncurry (cong₂ _,_) (Prod.map₂ (fromEqual ------------------------------------------------------------------------ -- projection of the k-th component --- To know at which Set level the k-th projection out of an n-ary product --- lives, we need to extract said level, by induction on k. +-- To know at which Set level the k-th projection out of an n-ary +-- product lives, we need to extract said level, by induction on k. Levelₙ : ∀ {n} → Levels n → Fin n → Level Levelₙ (l , _) zero = l @@ -157,10 +158,11 @@ Projₙ : ∀ {n ls} → Sets n ls → ∀ k → Set (Levelₙ ls k) Projₙ (a , _) zero = a Projₙ (_ , as) (suc k) = Projₙ as k --- Finally, provided a Product of these sets, we can extract the k-th value. --- `projₙ` takes both `n` and `k` explicitly because we expect the user will --- be using a concrete `k` (potentially manufactured using `Data.Fin`'s `#_`) --- and it will not be possible to infer `n` from it. +-- Finally, provided a Product of these sets, we can extract the k-th +-- value. `projₙ` takes both `n` and `k` explicitly because we expect +-- the user will be using a concrete `k` (potentially manufactured +-- using `Data.Fin`'s `#_`) and it will not be possible to infer `n` +-- from it. projₙ : ∀ n {ls} {as : Sets n ls} k → Product n as → Projₙ as k projₙ 1 zero v = v diff --git a/src/Data/Rational/Base.agda b/src/Data/Rational/Base.agda index 666cac3dc9..53739b8571 100644 --- a/src/Data/Rational/Base.agda +++ b/src/Data/Rational/Base.agda @@ -143,7 +143,7 @@ toℚᵘ (mkℚ n d-1 _) = mkℚᵘ n d-1 fromℚᵘ : ℚᵘ → ℚ fromℚᵘ (mkℚᵘ n d-1) = n / suc d-1 ------------------------------------------------------------------------------- +------------------------------------------------------------------------ -- Some constants 0ℚ : ℚ @@ -202,11 +202,11 @@ nonPositive {p@(mkℚ _ _ _)} (*≤* p≤q) = ℚᵘ.nonPositive {toℚᵘ p} ( nonNegative : ∀ {p} → p ≥ 0ℚ → NonNegative p nonNegative {p@(mkℚ _ _ _)} (*≤* p≤q) = ℚᵘ.nonNegative {toℚᵘ p} (ℚᵘ.*≤* p≤q) ------------------------------------------------------------------------------- +------------------------------------------------------------------------ -- Operations on rationals --- For explanation of the `@record{}` annotations see notes in the equivalent --- place in `Data.Rational.Unnormalised.Base`. +-- For explanation of the `@record{}` annotations see notes in the +-- equivalent place in `Data.Rational.Unnormalised.Base`. infix 8 -_ 1/_ infixl 7 _*_ _÷_ _⊓_ diff --git a/src/Data/Rational/Unnormalised/Base.agda b/src/Data/Rational/Unnormalised/Base.agda index c03041650c..ec104895be 100644 --- a/src/Data/Rational/Unnormalised/Base.agda +++ b/src/Data/Rational/Unnormalised/Base.agda @@ -117,7 +117,7 @@ infixl 7 _/_ _/_ : (n : ℤ) (d : ℕ) .{{_ : ℕ.NonZero d}} → ℚᵘ n / suc d = mkℚᵘ n d ------------------------------------------------------------------------------- +------------------------------------------------------------------------ -- Some constants 0ℚᵘ : ℚᵘ @@ -190,24 +190,25 @@ nonNegative : ∀ {p} → p ≥ 0ℚᵘ → NonNegative p nonNegative {mkℚᵘ +0 _} (*≤* _) = _ nonNegative {mkℚᵘ +[1+ n ] _} (*≤* _) = _ ------------------------------------------------------------------------------- +------------------------------------------------------------------------ -- Operations on rationals --- Explanation for `@record{}` everywhere: combined with no-eta-equality on --- the record definition of ℚᵘ above, these annotations prevent the operations --- from automatically expanding unless their arguments are explicitly pattern --- matched on. +-- Explanation for `@record{}` everywhere: combined with no-eta-equality +-- on the record definition of ℚᵘ above, these annotations prevent the +-- operations from automatically expanding unless their arguments are +-- explicitly pattern matched on. -- --- For example prior to their addition, `p + q` would often be normalised by --- Agda to `(↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)`. While in this --- small example this isn't a big problem, it leads to an exponential blowup --- when you have large arithmetic expressions which would often choke --- both type-checking and the display code. For example, the normalised --- form of `p + q + r + s + t + u` would be ~300 lines long. +-- For example prior to their addition, `p + q` would often be +-- normalised by Agda to `(↥ p ℤ.* ↧ q ℤ.+ ↥ q ℤ.* ↧ p) / (↧ₙ p ℕ.* ↧ₙ q)`. +-- While in this small example this isn't a big problem, it leads to an +-- exponential blowup when you have large arithmetic expressions which +-- would often choke both type-checking and the display code. For +-- example, the normalised form of `p + q + r + s + t + u` would be +-- ~300 lines long. -- --- This is fundementally a problem with Agda, so if over-eager normalisation --- is ever fixed in Agda (e.g. with glued representation of terms) these --- annotations can be removed. +-- This is fundementally a problem with Agda, so if over-eager +-- normalisation is ever fixed in Agda (e.g. with glued representation +-- of terms) these annotations can be removed. infix 8 -_ 1/_ infixl 7 _*_ _÷_ _⊓_ diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index 6f0d490412..3c800a5a98 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -794,7 +794,7 @@ p≤p+q p q rewrite +-comm-≡ p q = p≤q+p p q +-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_ +-mono-<-≤ {p} {q} {r} p x) ≡ x fmapId (inj₁ x) = refl fmapId (inj₂ y) = refl @@ -35,9 +35,9 @@ private open RawMonad Sₗ.monad - -- Now, let's show that "pure" is a unit for >>=. We use Lift in exactly - -- the same way as above. The data (x : B) then needs to be "lifted" to - -- this new type (Lift B). + -- Now, let's show that "pure" is a unit for >>=. We use Lift in + -- exactly the same way as above. The data (x : B) then needs to be + -- "lifted" to this new type (Lift B). pureUnitL : ∀ {x : B} {f : Lift a B → A ⊎ (Lift a B)} → (pure (lift x) >>= f) ≡ f (lift x) pureUnitL = refl diff --git a/src/Data/Sum/Effectful/Left.agda b/src/Data/Sum/Effectful/Left.agda index d86a7de26f..6d0f453b7b 100644 --- a/src/Data/Sum/Effectful/Left.agda +++ b/src/Data/Sum/Effectful/Left.agda @@ -18,9 +18,9 @@ open import Effect.Applicative open import Effect.Monad open import Function.Base --- To minimize the universe level of the RawFunctor, we require that elements of --- B are "lifted" to a copy of B at a higher universe level (a ⊔ b). See the --- examples for how this is done. +-- To minimize the universe level of the RawFunctor, we require that +-- elements of B are "lifted" to a copy of B at a higher universe level +-- (a ⊔ b). See the examples for how this is done. ------------------------------------------------------------------------ -- Left-biased monad instance for _⊎_ diff --git a/src/Data/Sum/Effectful/Left/Transformer.agda b/src/Data/Sum/Effectful/Left/Transformer.agda index cb45478f11..2d12a229fa 100644 --- a/src/Data/Sum/Effectful/Left/Transformer.agda +++ b/src/Data/Sum/Effectful/Left/Transformer.agda @@ -22,9 +22,9 @@ private variable M : Set (a ⊔ b) → Set (a ⊔ b) --- To minimize the universe level of the RawFunctor, we require that elements of --- B are "lifted" to a copy of B at a higher universe level (a ⊔ b). See the --- examples for how this is done. +-- To minimize the universe level of the RawFunctor, we require that +-- elements of B are "lifted" to a copy of B at a higher universe level +-- (a ⊔ b). See the examples for how this is done. open import Data.Sum.Effectful.Left A b using (Sumₗ) diff --git a/src/Data/Sum/Effectful/Right/Transformer.agda b/src/Data/Sum/Effectful/Right/Transformer.agda index 8fffb29c80..576d6fb379 100644 --- a/src/Data/Sum/Effectful/Right/Transformer.agda +++ b/src/Data/Sum/Effectful/Right/Transformer.agda @@ -22,9 +22,9 @@ private variable M : Set (a ⊔ b) → Set (a ⊔ b) --- To minimize the universe level of the RawFunctor, we require that elements of --- B are "lifted" to a copy of B at a higher universe level (a ⊔ b). See the --- examples for how this is done. +-- To minimize the universe level of the RawFunctor, we require that +-- elements of B are "lifted" to a copy of B at a higher universe level +-- (a ⊔ b). See the examples for how this is done. open import Data.Sum.Effectful.Right a B using (Sumᵣ) diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda index 34c676bcbb..36b2731087 100644 --- a/src/Data/Sum/Relation/Binary/LeftOrder.agda +++ b/src/Data/Sum/Relation/Binary/LeftOrder.agda @@ -20,7 +20,7 @@ import Relation.Nullary.Decidable as Dec open import Relation.Binary open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) ----------------------------------------------------------------------- +------------------------------------------------------------------------ -- Definition infixr 1 _⊎-<_ @@ -32,7 +32,7 @@ data _⊎-<_ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} ₁∼₁ : ∀ {x y} (x∼₁y : x ∼₁ y) → (_∼₁_ ⊎-< _∼₂_) (inj₁ x) (inj₁ y) ₂∼₂ : ∀ {x y} (x∼₂y : x ∼₂ y) → (_∼₁_ ⊎-< _∼₂_) (inj₂ x) (inj₂ y) ----------------------------------------------------------------------- +------------------------------------------------------------------------ -- Some properties which are preserved by _⊎-<_ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} @@ -127,7 +127,7 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} ... | tri≈ x≮y x≈y x≯y = tri≈ (x≮y ∘ drop-inj₂) (inj₂ x≈y) (x≯y ∘ drop-inj₂) ... | tri> x≮y x≉y x>y = tri> (x≮y ∘ drop-inj₂) (x≉y ∘ PW.drop-inj₂) (₂∼₂ x>y) ----------------------------------------------------------------------- +------------------------------------------------------------------------ -- Some collections of properties which are preserved module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda index 23d10172c9..724b341c5e 100644 --- a/src/Data/Sum/Relation/Binary/Pointwise.agda +++ b/src/Data/Sum/Relation/Binary/Pointwise.agda @@ -20,7 +20,7 @@ open import Relation.Binary open import Relation.Binary.PropositionalEquality.Core as P using (_≡_) import Relation.Binary.PropositionalEquality.Properties as P ----------------------------------------------------------------------- +------------------------------------------------------------------------ -- Definition data Pointwise {a b c d r s} @@ -30,7 +30,7 @@ data Pointwise {a b c d r s} inj₁ : ∀ {a c} → R a c → Pointwise R S (inj₁ a) (inj₁ c) inj₂ : ∀ {b d} → S b d → Pointwise R S (inj₂ b) (inj₂ d) ----------------------------------------------------------------------- +------------------------------------------------------------------------ -- Relational properties module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} @@ -108,7 +108,7 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} (Pointwise ∼₁ ∼₂) Respects₂ (Pointwise ≈₁ ≈₂) ⊎-respects₂ (r₁ , l₁) (r₂ , l₂) = ⊎-respectsʳ r₁ r₂ , ⊎-respectsˡ l₁ l₂ ----------------------------------------------------------------------- +------------------------------------------------------------------------ -- Structures module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂} diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda index f2dec21b8c..d78e152b6d 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda @@ -244,7 +244,7 @@ module _ {V : Value v} where Any P (singleton k v l