From 0ad66afdac3a66ad5166ee26ffe895c46dd7e07e Mon Sep 17 00:00:00 2001 From: Saransh Chopra Date: Tue, 27 Jun 2023 12:56:35 -0400 Subject: [PATCH] More fixities --- CHANGELOG.md | 8 ++++++++ src/Codata/Guarded/Stream/Relation/Unary/All.agda | 2 ++ src/Foreign/Haskell/List/NonEmpty.agda | 2 ++ src/Function/Metric/Rational/Bundles.agda | 12 ++++++++++++ src/Level/Literals.agda | 2 ++ src/Relation/Binary/Construct/Union.agda | 2 ++ .../HeterogeneousEquality/Quotients/Examples.agda | 2 ++ src/Relation/Binary/Indexed/Homogeneous/Bundles.agda | 3 +++ src/Text/Regex/Search.agda | 2 ++ 9 files changed, 35 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index b7b0f3f225..5728d4b6bf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -112,6 +112,14 @@ Bug-fixes infix 4 _≈∙_ (Relation.Binary.Construct.Add.Point.Equality) infix 4 _≤⁺_ _≤⊤⁺ (Relation.Binary.Construct.Add.Supremum.NonStrict) infixr 5 _∷ʳ_ (Relation.Binary.Construct.Closure.Transitive) + infixr 5 _∷_ (Codata.Guarded.Stream.Relation.Unary.All) + infixr 5 _∷_ (Foreign.Haskell.List.NonEmpty) + infix 4 _≈_ (Function.Metric.Rational.Bundles) + infixl 6 _ℕ+_ (Level.Literals) + infixr 6 _∪_ (Relation.Binary.Construct.Union) + infixl 6 _+ℤ_ (Relation.Binary.HeterogeneousEquality.Quotients.Examples) + infix 4 _≉_ _≈ᵢ_ _≤ᵢ_ (Relation.Binary.Indexed.Homogeneous.Bundles) + infixr 5 _∷ᴹ_ _∷⁻¹ᴹ_ (Text.Regex.Search) ``` * In `System.Exit`, the `ExitFailure` constructor is now carrying an integer diff --git a/src/Codata/Guarded/Stream/Relation/Unary/All.agda b/src/Codata/Guarded/Stream/Relation/Unary/All.agda index c69ff9124b..ad87a7e589 100644 --- a/src/Codata/Guarded/Stream/Relation/Unary/All.agda +++ b/src/Codata/Guarded/Stream/Relation/Unary/All.agda @@ -20,6 +20,8 @@ private P Q R : Pred A p xs : Stream A +infixr 5 _∷_ + record All (P : Pred A ℓ) (as : Stream A) : Set ℓ where coinductive constructor _∷_ diff --git a/src/Foreign/Haskell/List/NonEmpty.agda b/src/Foreign/Haskell/List/NonEmpty.agda index a36a1fc415..93e01e561f 100644 --- a/src/Foreign/Haskell/List/NonEmpty.agda +++ b/src/Foreign/Haskell/List/NonEmpty.agda @@ -25,5 +25,7 @@ private data NonEmpty (A : Set a) : Set a where _∷_ : A → List A → NonEmpty A +infixr 5 _∷_ + {-# FOREIGN GHC type AgdaNonEmpty l a = NE.NonEmpty a #-} {-# COMPILE GHC NonEmpty = data AgdaNonEmpty ((NE.:|)) #-} diff --git a/src/Function/Metric/Rational/Bundles.agda b/src/Function/Metric/Rational/Bundles.agda index 89067d2718..bdea51d507 100644 --- a/src/Function/Metric/Rational/Bundles.agda +++ b/src/Function/Metric/Rational/Bundles.agda @@ -34,6 +34,8 @@ record ProtoMetric a ℓ : Set (suc (a ⊔ ℓ)) where d : DistanceFunction Carrier isProtoMetric : IsProtoMetric _≈_ d + infix 4 _≈_ + open IsProtoMetric isProtoMetric public ------------------------------------------------------------------------ @@ -46,6 +48,8 @@ record PreMetric a ℓ : Set (suc (a ⊔ ℓ)) where d : DistanceFunction Carrier isPreMetric : IsPreMetric _≈_ d + infix 4 _≈_ + open IsPreMetric isPreMetric public protoMetric : ProtoMetric a ℓ @@ -63,6 +67,8 @@ record QuasiSemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where d : DistanceFunction Carrier isQuasiSemiMetric : IsQuasiSemiMetric _≈_ d + infix 4 _≈_ + open IsQuasiSemiMetric isQuasiSemiMetric public preMetric : PreMetric a ℓ @@ -83,6 +89,8 @@ record SemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where d : DistanceFunction Carrier isSemiMetric : IsSemiMetric _≈_ d + infix 4 _≈_ + open IsSemiMetric isSemiMetric public quasiSemiMetric : QuasiSemiMetric a ℓ @@ -103,6 +111,8 @@ record Metric a ℓ : Set (suc (a ⊔ ℓ)) where d : DistanceFunction Carrier isMetric : IsMetric _≈_ d + infix 4 _≈_ + open IsMetric isMetric public semiMetric : SemiMetric a ℓ @@ -123,6 +133,8 @@ record UltraMetric a ℓ : Set (suc (a ⊔ ℓ)) where d : DistanceFunction Carrier isUltraMetric : IsUltraMetric _≈_ d + infix 4 _≈_ + open IsUltraMetric isUltraMetric public semiMetric : SemiMetric a ℓ diff --git a/src/Level/Literals.agda b/src/Level/Literals.agda index 8e3eebb4e5..d1ac0f7ac4 100644 --- a/src/Level/Literals.agda +++ b/src/Level/Literals.agda @@ -15,6 +15,8 @@ open import Level using (Level; 0ℓ) -- Increase a Level by a number of sucs. +infixl 6 _ℕ+_ + _ℕ+_ : ℕ → Level → Level zero ℕ+ ℓ = ℓ suc n ℕ+ ℓ = Level.suc (n ℕ+ ℓ) diff --git a/src/Relation/Binary/Construct/Union.agda b/src/Relation/Binary/Construct/Union.agda index 3abd3ffe42..2b70ce8500 100644 --- a/src/Relation/Binary/Construct/Union.agda +++ b/src/Relation/Binary/Construct/Union.agda @@ -24,6 +24,8 @@ private ------------------------------------------------------------------------ -- Definition +infixr 6 _∪_ + _∪_ : REL A B ℓ₁ → REL A B ℓ₂ → REL A B (ℓ₁ ⊔ ℓ₂) L ∪ R = λ i j → L i j ⊎ R i j diff --git a/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda b/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda index c7bddf4a5a..fb1db6b9fb 100644 --- a/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda +++ b/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda @@ -82,6 +82,8 @@ module Integers (quot : Quotients 0ℓ 0ℓ) where module _ (ext : ∀ {a b} {A : Set a} {B₁ B₂ : A → Set b} {f₁ : ∀ a → B₁ a} {f₂ : ∀ a → B₂ a} → (∀ a → f₁ a ≅ f₂ a) → f₁ ≅ f₂) where + infixl 6 _+ℤ_ + _+ℤ_ : ℤ → ℤ → ℤ _+ℤ_ = Properties₂.lift₂ ext Int Int (λ i j → abs (i +² j)) $ λ {a} {b} {c} p p′ → compat-abs (+²-cong {a} {b} {c} p p′) diff --git a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda index 670949c138..fd83521783 100644 --- a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda +++ b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda @@ -39,6 +39,8 @@ record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where Carrier : Set _ Carrier = ∀ i → Carrierᵢ i + infix 4 _≉_ + _≈_ : B.Rel Carrier _ _≈_ = Lift Carrierᵢ _≈ᵢ_ @@ -103,6 +105,7 @@ record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ : record IndexedPoset {i} (I : Set i) c ℓ₁ ℓ₂ : Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where + infix 4 _≈ᵢ_ _≤ᵢ_ field Carrierᵢ : I → Set c _≈ᵢ_ : IRel Carrierᵢ ℓ₁ diff --git a/src/Text/Regex/Search.agda b/src/Text/Regex/Search.agda index af10c2784a..c802768e38 100644 --- a/src/Text/Regex/Search.agda +++ b/src/Text/Regex/Search.agda @@ -87,6 +87,8 @@ module Prefix where []⁻¹ᴹ : ∀ {e} → Match (Prefix _≡_) [] e → [] ∈ e []⁻¹ᴹ (mkMatch .[] p []) = p + infixr 5 _∷ᴹ_ _∷⁻¹ᴹ_ + _∷ᴹ_ : ∀ {xs e} x → Match (Prefix _≡_) xs (eat x e) → Match (Prefix _≡_) (x ∷ xs) e x ∷ᴹ (mkMatch ys ys∈e\x ys≤xs) = mkMatch (x ∷ ys) (eat-sound x _ ys∈e\x) (refl ∷ ys≤xs)