diff --git a/CHANGELOG.md b/CHANGELOG.md index e33d919313..13f0b0f20f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -31,51 +31,80 @@ Bug-fixes * The following operators were missing a fixity declaration, which has now been fixed - - ``` - infix -1 _$ⁿ_ (Data.Vec.N-ary) - infix 4 _≋_ (Data.Vec.Functional.Relation.Binary.Equality.Setoid) - infix 4 _≟_ (Reflection.AST.Definition) - infix 4 _≡ᵇ_ (Reflection.AST.Literal) - infix 4 _≈?_ _≟_ _≈_ (Reflection.AST.Meta) - infix 4 _≈?_ _≟_ _≈_ (Reflection.AST.Name) - infix 4 _≟-Telescope_ (Reflection.AST.Term) - infix 4 _≟_ (Reflection.AST.Argument.Information) - infix 4 _≟_ (Reflection.AST.Argument.Modality) - infix 4 _≟_ (Reflection.AST.Argument.Quantity) - infix 4 _≟_ (Reflection.AST.Argument.Relevance) - infix 4 _≟_ (Reflection.AST.Argument.Visibility) - infixr 8 _^_ (Function.Endomorphism.Propositional) - infixr 8 _^_ (Function.Endomorphism.Setoid) - infix 4 _≃_ (Function.HalfAdjointEquivalence) - infix 4 _≈_ _≈ᵢ_ _≤_ (Function.Metric.Bundles) - infixl 6 _∙_ (Function.Metric.Bundles) - infix 4 _≈_ (Function.Metric.Nat.Bundles) - infix 3 _←_ _↢_ (Function.Related) - - infix 4 _ℕ<_ _ℕ≤infinity _ℕ≤_ (Codata.Sized.Conat) - infix 6 _ℕ+_ _+ℕ_ (Codata.Sized.Conat) - infixl 4 _+ _* (Data.List.Kleene.Base) - infixr 4 _++++_ _+++*_ _*+++_ _*++*_ (Data.List.Kleene.Base) - infix 4 _[_]* _[_]+ (Data.List.Kleene.Base) - infix 4 _≢∈_ (Data.List.Membership.Propositional) - infixr 5 _`∷_ (Data.List.Reflection) - infix 4 _≡?_ (Data.List.Relation.Binary.Equality.DecPropositional) - infixr 5 _++ᵖ_ (Data.List.Relation.Binary.Prefix.Heterogeneous) - infixr 5 _++ˢ_ (Data.List.Relation.Binary.Suffix.Heterogeneous) - infixr 5 _++_ _++[] (Data.List.Relation.Ternary.Appending.Propositional) - infixr 5 _∷=_ (Data.List.Relation.Unary.Any) - infixr 5 _++_ (Data.List.Ternary.Appending) - infixr 2 _×-⇔_ _×-↣_ _×-↞_ _×-↠_ _×-↔_ _×-cong_ (Data.Product.Function.NonDependent.Propositional) - infixr 2 _×-⟶_ (Data.Product.Function.NonDependent.Setoid) - infixr 2 _×-equivalence_ _×-injection_ _×-left-inverse_ (Data.Product.Function.NonDependent.Setoid) - infixr 2 _×-surjection_ _×-inverse_ (Data.Product.Function.NonDependent.Setoid) - infixr 1 _⊎-⇔_ _⊎-↣_ _⊎-↞_ _⊎-↠_ _⊎-↔_ _⊎-cong_ (Data.Sum.Function.Propositional) - infixr 1 _⊎-⟶_ (Data.Sum.Function.Setoid) - infixr 1 _⊎-equivalence_ _⊎-injection_ _⊎-left-inverse_ (Data.Sum.Function.Setoid) - infixr 1 _⊎-surjection_ _⊎-inverse_ (Data.Sum.Function.Setoid) - infix 8 _⁻¹ (Data.Parity.Base) - infixr 5 _`∷_ (Data.Vec.Reflection) - infixr 5 _∷=_ (Data.Vec.Membership.Setoid) + ``` + infixr 5 _∷_ (Codata.Guarded.Stream) + infix 4 _[_] (Codata.Guarded.Stream) + infixr 5 _∷_ (Codata.Guarded.Stream.Relation.Binary.Pointwise) + infix 4 _≈∞_ (Codata.Guarded.Stream.Relation.Binary.Pointwise) + infixr 5 _∷_ (Codata.Musical.Colist) + infix 4 _≈_ (Codata.Musical.Conat) + infixr 5 _∷_ (Codata.Musical.Colist.Bisimilarity) + infixr 5 _∷_ (Codata.Musical.Colist.Relation.Unary.All) + infixr 5 _∷_ (Codata.Sized.Colist) + infixr 5 _∷_ (Codata.Sized.Covec) + infixr 5 _∷_ (Codata.Sized.Cowriter) + infixl 1 _>>=_ (Codata.Sized.Cowriter) + infixr 5 _∷_ (Codata.Sized.Stream) + infixr 5 _∷_ (Codata.Sized.Colist.Bisimilarity) + infix 4 _ℕ≤?_ (Codata.Sized.Conat.Properties) + infixr 5 _∷_ (Codata.Sized.Covec.Bisimilarity) + infixr 5 _∷_ (Codata.Sized.Cowriter.Bisimilarity) + infixr 5 _∷_ (Codata.Sized.Stream.Bisimilarity) + infixr 8 _⇒_ _⊸_ (Data.Container.Core) + infixr -1 _<$>_ _<*>_ (Data.Container.FreeMonad) + infixl 1 _>>=_ (Data.Container.FreeMonad) + infix 5 _▷_ (Data.Container.Indexed) + infix 4 _≈_ (Data.Float.Base) + infixl 7 _⊓′_ (Data.Nat.Base) + infixl 6 _⊔′_ (Data.Nat.Base) + infixr 8 _^_ (Data.Nat.Base) + infix 4 _!≢0 _!*_!≢0 (Data.Nat.Properties) + infix 4 _≃?_ (Data.Rational.Unnormalised.Properties) + infix 4 _≈ₖᵥ_ (Data.Tree.AVL.Map.Membership.Propositional) + infix 4 _<_ (Induction.WellFounded) + infix -1 _$ⁿ_ (Data.Vec.N-ary) + infix 4 _≋_ (Data.Vec.Functional.Relation.Binary.Equality.Setoid) + infix 4 _≟_ (Reflection.AST.Definition) + infix 4 _≡ᵇ_ (Reflection.AST.Literal) + infix 4 _≈?_ _≟_ _≈_ (Reflection.AST.Meta) + infix 4 _≈?_ _≟_ _≈_ (Reflection.AST.Name) + infix 4 _≟-Telescope_ (Reflection.AST.Term) + infix 4 _≟_ (Reflection.AST.Argument.Information) + infix 4 _≟_ (Reflection.AST.Argument.Modality) + infix 4 _≟_ (Reflection.AST.Argument.Quantity) + infix 4 _≟_ (Reflection.AST.Argument.Relevance) + infix 4 _≟_ (Reflection.AST.Argument.Visibility) + infixr 8 _^_ (Function.Endomorphism.Propositional) + infixr 8 _^_ (Function.Endomorphism.Setoid) + infix 4 _≃_ (Function.HalfAdjointEquivalence) + infix 4 _≈_ _≈ᵢ_ _≤_ (Function.Metric.Bundles) + infixl 6 _∙_ (Function.Metric.Bundles) + infix 4 _≈_ (Function.Metric.Nat.Bundles) + infix 3 _←_ _↢_ (Function.Related) + infix 4 _ℕ<_ _ℕ≤infinity _ℕ≤_ (Codata.Sized.Conat) + infix 6 _ℕ+_ _+ℕ_ (Codata.Sized.Conat) + infixl 4 _+ _* (Data.List.Kleene.Base) + infixr 4 _++++_ _+++*_ _*+++_ _*++*_ (Data.List.Kleene.Base) + infix 4 _[_]* _[_]+ (Data.List.Kleene.Base) + infix 4 _≢∈_ (Data.List.Membership.Propositional) + infixr 5 _`∷_ (Data.List.Reflection) + infix 4 _≡?_ (Data.List.Relation.Binary.Equality.DecPropositional) + infixr 5 _++ᵖ_ (Data.List.Relation.Binary.Prefix.Heterogeneous) + infixr 5 _++ˢ_ (Data.List.Relation.Binary.Suffix.Heterogeneous) + infixr 5 _++_ _++[] (Data.List.Relation.Ternary.Appending.Propositional) + infixr 5 _∷=_ (Data.List.Relation.Unary.Any) + infixr 5 _++_ (Data.List.Ternary.Appending) + infixr 2 _×-⇔_ _×-↣_ _×-↞_ _×-↠_ _×-↔_ _×-cong_ (Data.Product.Function.NonDependent.Propositional) + infixr 2 _×-⟶_ (Data.Product.Function.NonDependent.Setoid) + infixr 2 _×-equivalence_ _×-injection_ _×-left-inverse_ (Data.Product.Function.NonDependent.Setoid) + infixr 2 _×-surjection_ _×-inverse_ (Data.Product.Function.NonDependent.Setoid) + infixr 1 _⊎-⇔_ _⊎-↣_ _⊎-↞_ _⊎-↠_ _⊎-↔_ _⊎-cong_ (Data.Sum.Function.Propositional) + infixr 1 _⊎-⟶_ (Data.Sum.Function.Setoid) + infixr 1 _⊎-equivalence_ _⊎-injection_ _⊎-left-inverse_ (Data.Sum.Function.Setoid) + infixr 1 _⊎-surjection_ _⊎-inverse_ (Data.Sum.Function.Setoid) + infix 8 _⁻¹ (Data.Parity.Base) + infixr 5 _`∷_ (Data.Vec.Reflection) + infixr 5 _∷=_ (Data.Vec.Membership.Setoid) ``` * In `System.Exit`, the `ExitFailure` constructor is now carrying an integer diff --git a/src/Codata/Guarded/Stream.agda b/src/Codata/Guarded/Stream.agda index 88c5c5fec5..6024525cb4 100644 --- a/src/Codata/Guarded/Stream.agda +++ b/src/Codata/Guarded/Stream.agda @@ -28,6 +28,8 @@ private ------------------------------------------------------------------------ -- Type +infixr 5 _∷_ + record Stream (A : Set a) : Set a where coinductive constructor _∷_ @@ -69,6 +71,8 @@ lookup : Stream A → ℕ → A lookup xs zero = head xs lookup xs (suc n) = lookup (tail xs) n +infix 4 _[_] + _[_] : Stream A → ℕ → A _[_] = lookup diff --git a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda index 8f829297a0..c2d44f8145 100644 --- a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda +++ b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda @@ -25,6 +25,8 @@ private ------------------------------------------------------------------------ -- Bisimilarity +infixr 5 _∷_ + record Pointwise (_∼_ : REL A B ℓ) (as : Stream A) (bs : Stream B) : Set ℓ where coinductive constructor _∷_ @@ -191,4 +193,6 @@ module pw-Reasoning (S : Setoid a ℓ) where module ≈-Reasoning {a} {A : Set a} where open pw-Reasoning (P.setoid A) public + + infix 4 _≈∞_ _≈∞_ = `Pointwise∞ diff --git a/src/Codata/Musical/Colist.agda b/src/Codata/Musical/Colist.agda index c218a7f023..2ec01be70f 100644 --- a/src/Codata/Musical/Colist.agda +++ b/src/Codata/Musical/Colist.agda @@ -215,6 +215,8 @@ data Finite {A : Set a} : Colist A → Set a where [] : Finite [] _∷_ : ∀ x {xs} (fin : Finite (♭ xs)) → Finite (x ∷ xs) +infixr 5 _∷_ + module Finite-injective where ∷-injective : ∀ {x : A} {xs p q} → (Finite (x ∷ xs) ∋ x ∷ p) ≡ x ∷ q → p ≡ q diff --git a/src/Codata/Musical/Colist/Bisimilarity.agda b/src/Codata/Musical/Colist/Bisimilarity.agda index 8bcf5e5169..64a0c37d9c 100644 --- a/src/Codata/Musical/Colist/Bisimilarity.agda +++ b/src/Codata/Musical/Colist/Bisimilarity.agda @@ -27,6 +27,8 @@ data _≈_ {A : Set a} : Rel (Colist A) a where [] : [] ≈ [] _∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys +infixr 5 _∷_ + -- The equality relation forms a setoid. setoid : Set a → Setoid _ _ diff --git a/src/Codata/Musical/Colist/Relation/Unary/All.agda b/src/Codata/Musical/Colist/Relation/Unary/All.agda index df997252c3..ce937dc2b6 100644 --- a/src/Codata/Musical/Colist/Relation/Unary/All.agda +++ b/src/Codata/Musical/Colist/Relation/Unary/All.agda @@ -23,3 +23,5 @@ private data All {A : Set a} (P : Pred A p) : Pred (Colist A) (a ⊔ p) where [] : All P [] _∷_ : ∀ {x xs} (px : P x) (pxs : ∞ (All P (♭ xs))) → All P (x ∷ xs) + +infixr 5 _∷_ diff --git a/src/Codata/Musical/Conat.agda b/src/Codata/Musical/Conat.agda index 2d598fd75c..f8c1490a40 100644 --- a/src/Codata/Musical/Conat.agda +++ b/src/Codata/Musical/Conat.agda @@ -34,6 +34,8 @@ fromℕ-injective {suc m} {suc n} eq = P.cong suc (fromℕ-injective (P.cong pre ------------------------------------------------------------------------ -- Equality +infix 4 _≈_ + data _≈_ : Coℕ → Coℕ → Set where zero : zero ≈ zero suc : ∀ {m n} (m≈n : ∞ (♭ m ≈ ♭ n)) → suc m ≈ suc n diff --git a/src/Codata/Sized/Colist.agda b/src/Codata/Sized/Colist.agda index c090565c33..4f916fbc68 100644 --- a/src/Codata/Sized/Colist.agda +++ b/src/Codata/Sized/Colist.agda @@ -42,6 +42,8 @@ data Colist (A : Set a) (i : Size) : Set a where [] : Colist A i _∷_ : A → Thunk (Colist A) i → Colist A i +infixr 5 _∷_ + ------------------------------------------------------------------------ -- Relationship to Cowriter. diff --git a/src/Codata/Sized/Colist/Bisimilarity.agda b/src/Codata/Sized/Colist/Bisimilarity.agda index 9e626a5315..0a9f76306b 100644 --- a/src/Codata/Sized/Colist/Bisimilarity.agda +++ b/src/Codata/Sized/Colist/Bisimilarity.agda @@ -32,6 +32,8 @@ data Bisim {A : Set a} {B : Set b} (R : REL A B r) (i : Size) : _∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R) i xs ys → Bisim R i (x ∷ xs) (y ∷ ys) +infixr 5 _∷_ + module _ {R : Rel A r} where reflexive : Reflexive R → Reflexive (Bisim R i) diff --git a/src/Codata/Sized/Conat/Properties.agda b/src/Codata/Sized/Conat/Properties.agda index b2649fb38a..43d5662a9a 100644 --- a/src/Codata/Sized/Conat/Properties.agda +++ b/src/Codata/Sized/Conat/Properties.agda @@ -29,6 +29,8 @@ private sℕ≤s⁻¹ : ∀ {m n} → suc m ℕ≤ suc n → m ℕ≤ n .force sℕ≤s⁻¹ (sℕ≤s p) = p +infix 4 _ℕ≤?_ + _ℕ≤?_ : Decidable _ℕ≤_ zero ℕ≤? n = yes zℕ≤n suc m ℕ≤? zero = no (λ ()) diff --git a/src/Codata/Sized/Covec.agda b/src/Codata/Sized/Covec.agda index 85b7a9e63e..01e01f2df0 100644 --- a/src/Codata/Sized/Covec.agda +++ b/src/Codata/Sized/Covec.agda @@ -29,6 +29,8 @@ data Covec (A : Set a) (i : Size) : Conat ∞ → Set a where [] : Covec A i zero _∷_ : ∀ {n} → A → Thunk (λ i → Covec A i (n .force)) i → Covec A i (suc n) +infixr 5 _∷_ + head : ∀ {n i} → Covec A i (suc n) → A head (x ∷ _) = x diff --git a/src/Codata/Sized/Covec/Bisimilarity.agda b/src/Codata/Sized/Covec/Bisimilarity.agda index 3047816b44..cbe55ecbf7 100644 --- a/src/Codata/Sized/Covec/Bisimilarity.agda +++ b/src/Codata/Sized/Covec/Bisimilarity.agda @@ -22,6 +22,7 @@ data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) (i : Size) : _∷_ : ∀ {x y m n xs ys} → R x y → Thunk^R (λ i → Bisim R i (m .force) (n .force)) i xs ys → Bisim R i (suc m) (suc n) (x ∷ xs) (y ∷ ys) +infixr 5 _∷_ module _ {a r} {A : Set a} {R : A → A → Set r} where diff --git a/src/Codata/Sized/Cowriter.agda b/src/Codata/Sized/Cowriter.agda index 409fbe1f71..2a6ef961ec 100644 --- a/src/Codata/Sized/Cowriter.agda +++ b/src/Codata/Sized/Cowriter.agda @@ -39,6 +39,8 @@ data Cowriter (W : Set w) (A : Set a) (i : Size) : Set (a L.⊔ w) where [_] : A → Cowriter W A i _∷_ : W → Thunk (Cowriter W A) i → Cowriter W A i +infixr 5 _∷_ + ------------------------------------------------------------------------ -- Relationship to Delay. @@ -101,6 +103,8 @@ ap : ∀ {i} → Cowriter W (A → X) i → Cowriter W A i → Cowriter W X i ap [ f ] ca = map₂ f ca ap (w ∷ cf) ca = w ∷ λ where .force → ap (cf .force) ca +infixl 1 _>>=_ + _>>=_ : ∀ {i} → Cowriter W A i → (A → Cowriter W X i) → Cowriter W X i [ a ] >>= f = f a (w ∷ ca) >>= f = w ∷ λ where .force → ca .force >>= f diff --git a/src/Codata/Sized/Cowriter/Bisimilarity.agda b/src/Codata/Sized/Cowriter/Bisimilarity.agda index 823b7897ae..846101b538 100644 --- a/src/Codata/Sized/Cowriter/Bisimilarity.agda +++ b/src/Codata/Sized/Cowriter/Bisimilarity.agda @@ -33,6 +33,8 @@ data Bisim {V : Set v} {W : Set w} {A : Set a} {B : Set b} _∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R S) i xs ys → Bisim R S i (x ∷ xs) (y ∷ ys) +infixr 5 _∷_ + module _ {R : Rel W r} {S : Rel A s} (refl^R : Reflexive R) (refl^S : Reflexive S) where diff --git a/src/Codata/Sized/Stream.agda b/src/Codata/Sized/Stream.agda index 53e42aa87d..85cd886b5f 100644 --- a/src/Codata/Sized/Stream.agda +++ b/src/Codata/Sized/Stream.agda @@ -34,6 +34,8 @@ private data Stream (A : Set a) (i : Size) : Set a where _∷_ : A → Thunk (Stream A) i → Stream A i +infixr 5 _∷_ + ------------------------------------------------------------------------ -- Creating streams diff --git a/src/Codata/Sized/Stream/Bisimilarity.agda b/src/Codata/Sized/Stream/Bisimilarity.agda index 1675ec016a..737e73c306 100644 --- a/src/Codata/Sized/Stream/Bisimilarity.agda +++ b/src/Codata/Sized/Stream/Bisimilarity.agda @@ -30,6 +30,8 @@ data Bisim {A : Set a} {B : Set b} (R : REL A B r) i : _∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R) i xs ys → Bisim R i (x ∷ xs) (y ∷ ys) +infixr 5 _∷_ + module _ {R : Rel A r} where reflexive : Reflexive R → Reflexive (Bisim R i) diff --git a/src/Data/Container/Core.agda b/src/Data/Container/Core.agda index 9d07031d20..22b26955d8 100644 --- a/src/Data/Container/Core.agda +++ b/src/Data/Container/Core.agda @@ -38,6 +38,8 @@ map f = Prod.map₂ (f ∘_) -- Representation of container morphisms. +infixr 8 _⇒_ _⊸_ + record _⇒_ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) : Set (s₁ ⊔ s₂ ⊔ p₁ ⊔ p₂) where constructor _▷_ diff --git a/src/Data/Container/FreeMonad.agda b/src/Data/Container/FreeMonad.agda index d1853782c9..1d206a4b87 100644 --- a/src/Data/Container/FreeMonad.agda +++ b/src/Data/Container/FreeMonad.agda @@ -103,6 +103,9 @@ module _ {P : Set ℓ} foldr : C ⋆ X → P foldr = induction (Function.const P) algP (algI ∘ -,_ ∘ □.proof) +infixr -1 _<$>_ _<*>_ +infixl 1 _>>=_ + _<$>_ : (X → Y) → C ⋆ X → C ⋆ Y f <$> t = foldr (pure ∘ f) impure t diff --git a/src/Data/Container/Indexed.agda b/src/Data/Container/Indexed.agda index 752f55c2a7..a5b17d2aab 100644 --- a/src/Data/Container/Indexed.agda +++ b/src/Data/Container/Indexed.agda @@ -31,6 +31,8 @@ open Container public -- Abbreviation for the commonly used level one version of indexed -- containers. +infix 5 _▷_ + _▷_ : Set → Set → Set₁ I ▷ O = Container I O zero zero @@ -103,6 +105,8 @@ module _ {i₁ i₂ o₁ o₂} module _ {i o c r} {I : Set i} {O : Set o} where + infixr 8 _⇒_ _⊸_ _⇒C_ + _⇒_ : B.Rel (Container I O c r) _ C₁ ⇒ C₂ = C₁ ⇒[ ⟨id⟩ / ⟨id⟩ ] C₂ diff --git a/src/Data/Float/Base.agda b/src/Data/Float/Base.agda index edc8b4943f..d09a5a811b 100644 --- a/src/Data/Float/Base.agda +++ b/src/Data/Float/Base.agda @@ -65,5 +65,7 @@ open import Agda.Builtin.Float public ; primFloatATanh to atanh ) +infix 4 _≈_ + _≈_ : Rel Float _ _≈_ = _≡_ on Maybe.map Word.toℕ ∘ toWord diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 1e2db666b8..4920e7751e 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -132,8 +132,8 @@ pred : ℕ → ℕ pred n = n ∸ 1 infix 8 _! -infixl 7 _⊓_ _/_ _%_ -infixl 6 _+⋎_ _⊔_ +infixl 7 _⊓_ _⊓′_ _/_ _%_ +infixl 6 _+⋎_ _⊔_ _⊔′_ -- Argument-swapping addition. Used by Data.Vec._⋎_. @@ -192,6 +192,8 @@ parity (suc (suc n)) = parity n -- Naïve exponentiation +infixr 8 _^_ + _^_ : ℕ → ℕ → ℕ x ^ zero = 1 x ^ suc n = x * x ^ n diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 6ff1b1f38b..27725b98ad 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1948,6 +1948,8 @@ n≡⌈n+n/2⌉ (suc n′@(suc n)) = 1≤n! zero = ≤-refl 1≤n! (suc n) = *-mono-≤ (m≤m+n 1 n) (1≤n! n) +infix 4 _!≢0 _!*_!≢0 + _!≢0 : ∀ n → NonZero (n !) n !≢0 = >-nonZero (1≤n! n) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index d1eb0fe609..6f0d490412 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -91,6 +91,8 @@ drop-*≡* (*≡* eq) = eq ↥ z ℤ.* ↧ x ℤ.* ↧ y ∎)) where open ≡-Reasoning +infix 4 _≃?_ + _≃?_ : Decidable _≃_ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* ↧ p) diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional.agda b/src/Data/Tree/AVL/Map/Membership/Propositional.agda index a353ddf4ad..7e5d297025 100644 --- a/src/Data/Tree/AVL/Map/Membership/Propositional.agda +++ b/src/Data/Tree/AVL/Map/Membership/Propositional.agda @@ -49,6 +49,8 @@ private x x′ y y′ : V kx : Key × V +infix 4 _≈ₖᵥ_ + _≈ₖᵥ_ : Rel (Key × V) _ _≈ₖᵥ_ = _≈_ ×ᴿ _≡_ diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda index 5c88529d27..d580452f0f 100644 --- a/src/Induction/WellFounded.agda +++ b/src/Induction/WellFounded.agda @@ -184,6 +184,7 @@ module Lexicographic {A : Set a} {B : A → Set b} (RelA : Rel A ℓ₁) (RelB : ∀ x → Rel (B x) ℓ₂) where + infix 4 _<_ data _<_ : Rel (Σ A B) (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where left : ∀ {x₁ y₁ x₂ y₂} (x₁