Skip to content

Commit 657fa5a

Browse files
Saransh-cppplt-amy
Saransh-cpp
authored and
plt-amy
committed
More fixities for Data and Codata (#1989)
1 parent 48e3a34 commit 657fa5a

File tree

25 files changed

+131
-47
lines changed

25 files changed

+131
-47
lines changed

‎CHANGELOG.md

+74-45
Original file line numberDiff line numberDiff line change
@@ -31,51 +31,80 @@ Bug-fixes
3131

3232
* The following operators were missing a fixity declaration, which has now
3333
been fixed -
34-
```
35-
infix -1 _$ⁿ_ (Data.Vec.N-ary)
36-
infix 4 _≋_ (Data.Vec.Functional.Relation.Binary.Equality.Setoid)
37-
infix 4 _≟_ (Reflection.AST.Definition)
38-
infix 4 _≡ᵇ_ (Reflection.AST.Literal)
39-
infix 4 _≈?_ _≟_ _≈_ (Reflection.AST.Meta)
40-
infix 4 _≈?_ _≟_ _≈_ (Reflection.AST.Name)
41-
infix 4 _≟-Telescope_ (Reflection.AST.Term)
42-
infix 4 _≟_ (Reflection.AST.Argument.Information)
43-
infix 4 _≟_ (Reflection.AST.Argument.Modality)
44-
infix 4 _≟_ (Reflection.AST.Argument.Quantity)
45-
infix 4 _≟_ (Reflection.AST.Argument.Relevance)
46-
infix 4 _≟_ (Reflection.AST.Argument.Visibility)
47-
infixr 8 _^_ (Function.Endomorphism.Propositional)
48-
infixr 8 _^_ (Function.Endomorphism.Setoid)
49-
infix 4 _≃_ (Function.HalfAdjointEquivalence)
50-
infix 4 _≈_ _≈ᵢ_ _≤_ (Function.Metric.Bundles)
51-
infixl 6 _∙_ (Function.Metric.Bundles)
52-
infix 4 _≈_ (Function.Metric.Nat.Bundles)
53-
infix 3 _←_ _↢_ (Function.Related)
54-
55-
infix 4 _ℕ<_ _ℕ≤infinity _ℕ≤_ (Codata.Sized.Conat)
56-
infix 6 _ℕ+_ _+ℕ_ (Codata.Sized.Conat)
57-
infixl 4 _+ _* (Data.List.Kleene.Base)
58-
infixr 4 _++++_ _+++*_ _*+++_ _*++*_ (Data.List.Kleene.Base)
59-
infix 4 _[_]* _[_]+ (Data.List.Kleene.Base)
60-
infix 4 _≢∈_ (Data.List.Membership.Propositional)
61-
infixr 5 _`∷_ (Data.List.Reflection)
62-
infix 4 _≡?_ (Data.List.Relation.Binary.Equality.DecPropositional)
63-
infixr 5 _++ᵖ_ (Data.List.Relation.Binary.Prefix.Heterogeneous)
64-
infixr 5 _++ˢ_ (Data.List.Relation.Binary.Suffix.Heterogeneous)
65-
infixr 5 _++_ _++[] (Data.List.Relation.Ternary.Appending.Propositional)
66-
infixr 5 _∷=_ (Data.List.Relation.Unary.Any)
67-
infixr 5 _++_ (Data.List.Ternary.Appending)
68-
infixr 2 _×-⇔_ _×-↣_ _×-↞_ _×-↠_ _×-↔_ _×-cong_ (Data.Product.Function.NonDependent.Propositional)
69-
infixr 2 _×-⟶_ (Data.Product.Function.NonDependent.Setoid)
70-
infixr 2 _×-equivalence_ _×-injection_ _×-left-inverse_ (Data.Product.Function.NonDependent.Setoid)
71-
infixr 2 _×-surjection_ _×-inverse_ (Data.Product.Function.NonDependent.Setoid)
72-
infixr 1 _⊎-⇔_ _⊎-↣_ _⊎-↞_ _⊎-↠_ _⊎-↔_ _⊎-cong_ (Data.Sum.Function.Propositional)
73-
infixr 1 _⊎-⟶_ (Data.Sum.Function.Setoid)
74-
infixr 1 _⊎-equivalence_ _⊎-injection_ _⊎-left-inverse_ (Data.Sum.Function.Setoid)
75-
infixr 1 _⊎-surjection_ _⊎-inverse_ (Data.Sum.Function.Setoid)
76-
infix 8 _⁻¹ (Data.Parity.Base)
77-
infixr 5 _`∷_ (Data.Vec.Reflection)
78-
infixr 5 _∷=_ (Data.Vec.Membership.Setoid)
34+
```
35+
infixr 5 _∷_ (Codata.Guarded.Stream)
36+
infix 4 _[_] (Codata.Guarded.Stream)
37+
infixr 5 _∷_ (Codata.Guarded.Stream.Relation.Binary.Pointwise)
38+
infix 4 _≈∞_ (Codata.Guarded.Stream.Relation.Binary.Pointwise)
39+
infixr 5 _∷_ (Codata.Musical.Colist)
40+
infix 4 _≈_ (Codata.Musical.Conat)
41+
infixr 5 _∷_ (Codata.Musical.Colist.Bisimilarity)
42+
infixr 5 _∷_ (Codata.Musical.Colist.Relation.Unary.All)
43+
infixr 5 _∷_ (Codata.Sized.Colist)
44+
infixr 5 _∷_ (Codata.Sized.Covec)
45+
infixr 5 _∷_ (Codata.Sized.Cowriter)
46+
infixl 1 _>>=_ (Codata.Sized.Cowriter)
47+
infixr 5 _∷_ (Codata.Sized.Stream)
48+
infixr 5 _∷_ (Codata.Sized.Colist.Bisimilarity)
49+
infix 4 _ℕ≤?_ (Codata.Sized.Conat.Properties)
50+
infixr 5 _∷_ (Codata.Sized.Covec.Bisimilarity)
51+
infixr 5 _∷_ (Codata.Sized.Cowriter.Bisimilarity)
52+
infixr 5 _∷_ (Codata.Sized.Stream.Bisimilarity)
53+
infixr 8 _⇒_ _⊸_ (Data.Container.Core)
54+
infixr -1 _<$>_ _<*>_ (Data.Container.FreeMonad)
55+
infixl 1 _>>=_ (Data.Container.FreeMonad)
56+
infix 5 _▷_ (Data.Container.Indexed)
57+
infix 4 _≈_ (Data.Float.Base)
58+
infixl 7 _⊓′_ (Data.Nat.Base)
59+
infixl 6 _⊔′_ (Data.Nat.Base)
60+
infixr 8 _^_ (Data.Nat.Base)
61+
infix 4 _!≢0 _!*_!≢0 (Data.Nat.Properties)
62+
infix 4 _≃?_ (Data.Rational.Unnormalised.Properties)
63+
infix 4 _≈ₖᵥ_ (Data.Tree.AVL.Map.Membership.Propositional)
64+
infix 4 _<_ (Induction.WellFounded)
65+
infix -1 _$ⁿ_ (Data.Vec.N-ary)
66+
infix 4 _≋_ (Data.Vec.Functional.Relation.Binary.Equality.Setoid)
67+
infix 4 _≟_ (Reflection.AST.Definition)
68+
infix 4 _≡ᵇ_ (Reflection.AST.Literal)
69+
infix 4 _≈?_ _≟_ _≈_ (Reflection.AST.Meta)
70+
infix 4 _≈?_ _≟_ _≈_ (Reflection.AST.Name)
71+
infix 4 _≟-Telescope_ (Reflection.AST.Term)
72+
infix 4 _≟_ (Reflection.AST.Argument.Information)
73+
infix 4 _≟_ (Reflection.AST.Argument.Modality)
74+
infix 4 _≟_ (Reflection.AST.Argument.Quantity)
75+
infix 4 _≟_ (Reflection.AST.Argument.Relevance)
76+
infix 4 _≟_ (Reflection.AST.Argument.Visibility)
77+
infixr 8 _^_ (Function.Endomorphism.Propositional)
78+
infixr 8 _^_ (Function.Endomorphism.Setoid)
79+
infix 4 _≃_ (Function.HalfAdjointEquivalence)
80+
infix 4 _≈_ _≈ᵢ_ _≤_ (Function.Metric.Bundles)
81+
infixl 6 _∙_ (Function.Metric.Bundles)
82+
infix 4 _≈_ (Function.Metric.Nat.Bundles)
83+
infix 3 _←_ _↢_ (Function.Related)
84+
infix 4 _ℕ<_ _ℕ≤infinity _ℕ≤_ (Codata.Sized.Conat)
85+
infix 6 _ℕ+_ _+ℕ_ (Codata.Sized.Conat)
86+
infixl 4 _+ _* (Data.List.Kleene.Base)
87+
infixr 4 _++++_ _+++*_ _*+++_ _*++*_ (Data.List.Kleene.Base)
88+
infix 4 _[_]* _[_]+ (Data.List.Kleene.Base)
89+
infix 4 _≢∈_ (Data.List.Membership.Propositional)
90+
infixr 5 _`∷_ (Data.List.Reflection)
91+
infix 4 _≡?_ (Data.List.Relation.Binary.Equality.DecPropositional)
92+
infixr 5 _++ᵖ_ (Data.List.Relation.Binary.Prefix.Heterogeneous)
93+
infixr 5 _++ˢ_ (Data.List.Relation.Binary.Suffix.Heterogeneous)
94+
infixr 5 _++_ _++[] (Data.List.Relation.Ternary.Appending.Propositional)
95+
infixr 5 _∷=_ (Data.List.Relation.Unary.Any)
96+
infixr 5 _++_ (Data.List.Ternary.Appending)
97+
infixr 2 _×-⇔_ _×-↣_ _×-↞_ _×-↠_ _×-↔_ _×-cong_ (Data.Product.Function.NonDependent.Propositional)
98+
infixr 2 _×-⟶_ (Data.Product.Function.NonDependent.Setoid)
99+
infixr 2 _×-equivalence_ _×-injection_ _×-left-inverse_ (Data.Product.Function.NonDependent.Setoid)
100+
infixr 2 _×-surjection_ _×-inverse_ (Data.Product.Function.NonDependent.Setoid)
101+
infixr 1 _⊎-⇔_ _⊎-↣_ _⊎-↞_ _⊎-↠_ _⊎-↔_ _⊎-cong_ (Data.Sum.Function.Propositional)
102+
infixr 1 _⊎-⟶_ (Data.Sum.Function.Setoid)
103+
infixr 1 _⊎-equivalence_ _⊎-injection_ _⊎-left-inverse_ (Data.Sum.Function.Setoid)
104+
infixr 1 _⊎-surjection_ _⊎-inverse_ (Data.Sum.Function.Setoid)
105+
infix 8 _⁻¹ (Data.Parity.Base)
106+
infixr 5 _`∷_ (Data.Vec.Reflection)
107+
infixr 5 _∷=_ (Data.Vec.Membership.Setoid)
79108
```
80109

81110
* In `System.Exit`, the `ExitFailure` constructor is now carrying an integer

‎src/Codata/Guarded/Stream.agda

+4
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,8 @@ private
2828
------------------------------------------------------------------------
2929
-- Type
3030

31+
infixr 5 _∷_
32+
3133
record Stream (A : Set a) : Set a where
3234
coinductive
3335
constructor _∷_
@@ -69,6 +71,8 @@ lookup : Stream A → ℕ → A
6971
lookup xs zero = head xs
7072
lookup xs (suc n) = lookup (tail xs) n
7173

74+
infix 4 _[_]
75+
7276
_[_] : Stream A → ℕ → A
7377
_[_] = lookup
7478

‎src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda

+4
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,8 @@ private
2525
------------------------------------------------------------------------
2626
-- Bisimilarity
2727

28+
infixr 5 _∷_
29+
2830
record Pointwise (_∼_ : REL A B ℓ) (as : Stream A) (bs : Stream B) : Set ℓ where
2931
coinductive
3032
constructor _∷_
@@ -191,4 +193,6 @@ module pw-Reasoning (S : Setoid a ℓ) where
191193
module ≈-Reasoning {a} {A : Set a} where
192194

193195
open pw-Reasoning (P.setoid A) public
196+
197+
infix 4 _≈∞_
194198
_≈∞_ = `Pointwise∞

‎src/Codata/Musical/Colist.agda

+2
Original file line numberDiff line numberDiff line change
@@ -215,6 +215,8 @@ data Finite {A : Set a} : Colist A → Set a where
215215
[] : Finite []
216216
_∷_ : ∀ x {xs} (fin : Finite (♭ xs)) → Finite (x ∷ xs)
217217

218+
infixr 5 _∷_
219+
218220
module Finite-injective where
219221

220222
∷-injective : ∀ {x : A} {xs p q} → (Finite (x ∷ xs) ∋ x ∷ p) ≡ x ∷ q → p ≡ q

‎src/Codata/Musical/Colist/Bisimilarity.agda

+2
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,8 @@ data _≈_ {A : Set a} : Rel (Colist A) a where
2727
[] : [] ≈ []
2828
_∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys
2929

30+
infixr 5 _∷_
31+
3032
-- The equality relation forms a setoid.
3133

3234
setoid : Set a → Setoid _ _

‎src/Codata/Musical/Colist/Relation/Unary/All.agda

+2
Original file line numberDiff line numberDiff line change
@@ -23,3 +23,5 @@ private
2323
data All {A : Set a} (P : Pred A p) : Pred (Colist A) (a ⊔ p) where
2424
[] : All P []
2525
_∷_ : ∀ {x xs} (px : P x) (pxs : ∞ (All P (♭ xs))) → All P (x ∷ xs)
26+
27+
infixr 5 _∷_

‎src/Codata/Musical/Conat.agda

+2
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,8 @@ fromℕ-injective {suc m} {suc n} eq = P.cong suc (fromℕ-injective (P.cong pre
3434
------------------------------------------------------------------------
3535
-- Equality
3636

37+
infix 4 _≈_
38+
3739
data _≈_ : Coℕ → Coℕ → Set where
3840
zero : zero ≈ zero
3941
suc : ∀ {m n} (m≈n : ∞ (♭ m ≈ ♭ n)) → suc m ≈ suc n

‎src/Codata/Sized/Colist.agda

+2
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,8 @@ data Colist (A : Set a) (i : Size) : Set a where
4242
[] : Colist A i
4343
_∷_ : A → Thunk (Colist A) i → Colist A i
4444

45+
infixr 5 _∷_
46+
4547
------------------------------------------------------------------------
4648
-- Relationship to Cowriter.
4749

‎src/Codata/Sized/Colist/Bisimilarity.agda

+2
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,8 @@ data Bisim {A : Set a} {B : Set b} (R : REL A B r) (i : Size) :
3232
_∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R) i xs ys →
3333
Bisim R i (x ∷ xs) (y ∷ ys)
3434

35+
infixr 5 _∷_
36+
3537
module _ {R : Rel A r} where
3638

3739
reflexive : Reflexive R → Reflexive (Bisim R i)

‎src/Codata/Sized/Conat/Properties.agda

+2
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@ private
2929
sℕ≤s⁻¹ : ∀ {m n} → suc m ℕ≤ suc n → m ℕ≤ n .force
3030
sℕ≤s⁻¹ (sℕ≤s p) = p
3131

32+
infix 4 _ℕ≤?_
33+
3234
_ℕ≤?_ : Decidable _ℕ≤_
3335
zero ℕ≤? n = yes zℕ≤n
3436
suc m ℕ≤? zero = no (λ ())

‎src/Codata/Sized/Covec.agda

+2
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@ data Covec (A : Set a) (i : Size) : Conat ∞ → Set a where
2929
[] : Covec A i zero
3030
_∷_ : ∀ {n} → A → Thunk (λ i → Covec A i (n .force)) i → Covec A i (suc n)
3131

32+
infixr 5 _∷_
33+
3234
head : ∀ {n i} → Covec A i (suc n) → A
3335
head (x ∷ _) = x
3436

‎src/Codata/Sized/Covec/Bisimilarity.agda

+1
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) (i : Size) :
2222
_∷_ : ∀ {x y m n xs ys} → R x y → Thunk^R (λ i → Bisim R i (m .force) (n .force)) i xs ys →
2323
Bisim R i (suc m) (suc n) (x ∷ xs) (y ∷ ys)
2424

25+
infixr 5 _∷_
2526

2627
module _ {a r} {A : Set a} {R : A → A → Set r} where
2728

‎src/Codata/Sized/Cowriter.agda

+4
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,8 @@ data Cowriter (W : Set w) (A : Set a) (i : Size) : Set (a L.⊔ w) where
3939
[_] : A → Cowriter W A i
4040
_∷_ : W → Thunk (Cowriter W A) i → Cowriter W A i
4141

42+
infixr 5 _∷_
43+
4244
------------------------------------------------------------------------
4345
-- Relationship to Delay.
4446

@@ -101,6 +103,8 @@ ap : ∀ {i} → Cowriter W (A → X) i → Cowriter W A i → Cowriter W X i
101103
ap [ f ] ca = map₂ f ca
102104
ap (w ∷ cf) ca = w ∷ λ where .force → ap (cf .force) ca
103105

106+
infixl 1 _>>=_
107+
104108
_>>=_ : ∀ {i} → Cowriter W A i → (A → Cowriter W X i) → Cowriter W X i
105109
[ a ] >>= f = f a
106110
(w ∷ ca) >>= f = w ∷ λ where .force → ca .force >>= f

‎src/Codata/Sized/Cowriter/Bisimilarity.agda

+2
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,8 @@ data Bisim {V : Set v} {W : Set w} {A : Set a} {B : Set b}
3333
_∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R S) i xs ys →
3434
Bisim R S i (x ∷ xs) (y ∷ ys)
3535

36+
infixr 5 _∷_
37+
3638
module _ {R : Rel W r} {S : Rel A s}
3739
(refl^R : Reflexive R) (refl^S : Reflexive S) where
3840

‎src/Codata/Sized/Stream.agda

+2
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,8 @@ private
3434
data Stream (A : Set a) (i : Size) : Set a where
3535
_∷_ : A → Thunk (Stream A) i → Stream A i
3636

37+
infixr 5 _∷_
38+
3739
------------------------------------------------------------------------
3840
-- Creating streams
3941

‎src/Codata/Sized/Stream/Bisimilarity.agda

+2
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ data Bisim {A : Set a} {B : Set b} (R : REL A B r) i :
3030
_∷_ : ∀ {x y xs ys} → R x y → Thunk^R (Bisim R) i xs ys →
3131
Bisim R i (x ∷ xs) (y ∷ ys)
3232

33+
infixr 5 _∷_
34+
3335
module _ {R : Rel A r} where
3436

3537
reflexive : Reflexive R → Reflexive (Bisim R i)

‎src/Data/Container/Core.agda

+2
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,8 @@ map f = Prod.map₂ (f ∘_)
3838

3939
-- Representation of container morphisms.
4040

41+
infixr 8 _⇒_ _⊸_
42+
4143
record _⇒_ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂)
4244
: Set (s₁ ⊔ s₂ ⊔ p₁ ⊔ p₂) where
4345
constructor _▷_

‎src/Data/Container/FreeMonad.agda

+3
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,9 @@ module _ {P : Set ℓ}
103103
foldr : C ⋆ X → P
104104
foldr = induction (Function.const P) algP (algI ∘ -,_ ∘ □.proof)
105105

106+
infixr -1 _<$>_ _<*>_
107+
infixl 1 _>>=_
108+
106109
_<$>_ : (X → Y) → C ⋆ X → C ⋆ Y
107110
f <$> t = foldr (pure ∘ f) impure t
108111

‎src/Data/Container/Indexed.agda

+4
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,8 @@ open Container public
3131
-- Abbreviation for the commonly used level one version of indexed
3232
-- containers.
3333

34+
infix 5 _▷_
35+
3436
_▷_ : Set → Set → Set₁
3537
I ▷ O = Container I O zero zero
3638

@@ -103,6 +105,8 @@ module _ {i₁ i₂ o₁ o₂}
103105

104106
module _ {i o c r} {I : Set i} {O : Set o} where
105107

108+
infixr 8 _⇒_ _⊸_ _⇒C_
109+
106110
_⇒_ : B.Rel (Container I O c r) _
107111
C₁ ⇒ C₂ = C₁ ⇒[ ⟨id⟩ / ⟨id⟩ ] C₂
108112

‎src/Data/Float/Base.agda

+2
Original file line numberDiff line numberDiff line change
@@ -65,5 +65,7 @@ open import Agda.Builtin.Float public
6565
; primFloatATanh to atanh
6666
)
6767

68+
infix 4 _≈_
69+
6870
_≈_ : Rel Float _
6971
_≈_ = _≡_ on Maybe.map Word.toℕ ∘ toWord

‎src/Data/Nat/Base.agda

+4-2
Original file line numberDiff line numberDiff line change
@@ -132,8 +132,8 @@ pred : ℕ → ℕ
132132
pred n = n ∸ 1
133133

134134
infix 8 _!
135-
infixl 7 _⊓_ _/_ _%_
136-
infixl 6 _+⋎_ _⊔_
135+
infixl 7 _⊓_ _⊓′_ _/_ _%_
136+
infixl 6 _+⋎_ _⊔_ _⊔′_
137137

138138
-- Argument-swapping addition. Used by Data.Vec._⋎_.
139139

@@ -192,6 +192,8 @@ parity (suc (suc n)) = parity n
192192

193193
-- Naïve exponentiation
194194

195+
infixr 8 _^_
196+
195197
_^_ : ℕ → ℕ → ℕ
196198
x ^ zero = 1
197199
x ^ suc n = x * x ^ n

‎src/Data/Nat/Properties.agda

+2
Original file line numberDiff line numberDiff line change
@@ -1948,6 +1948,8 @@ n≡⌈n+n/2⌉ (suc n′@(suc n)) =
19481948
1≤n! zero = ≤-refl
19491949
1≤n! (suc n) = *-mono-≤ (m≤m+n 1 n) (1≤n! n)
19501950

1951+
infix 4 _!≢0 _!*_!≢0
1952+
19511953
_!≢0 : ∀ n → NonZero (n !)
19521954
n !≢0 = >-nonZero (1≤n! n)
19531955

‎src/Data/Rational/Unnormalised/Properties.agda

+2
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,8 @@ drop-*≡* (*≡* eq) = eq
9191
↥ z ℤ.* ↧ x ℤ.* ↧ y ∎))
9292
where open ≡-Reasoning
9393

94+
infix 4 _≃?_
95+
9496
_≃?_ : Decidable _≃_
9597
p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* ↧ p)
9698

‎src/Data/Tree/AVL/Map/Membership/Propositional.agda

+2
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,8 @@ private
4949
x x′ y y′ : V
5050
kx : Key × V
5151

52+
infix 4 _≈ₖᵥ_
53+
5254
_≈ₖᵥ_ : Rel (Key × V) _
5355
_≈ₖᵥ_ = _≈_ ×ᴿ _≡_
5456

‎src/Induction/WellFounded.agda

+1
Original file line numberDiff line numberDiff line change
@@ -184,6 +184,7 @@ module Lexicographic {A : Set a} {B : A → Set b}
184184
(RelA : Rel A ℓ₁)
185185
(RelB : ∀ x → Rel (B x) ℓ₂) where
186186

187+
infix 4 _<_
187188
data _<_ : Rel (Σ A B) (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
188189
left : ∀ {x₁ y₁ x₂ y₂} (x₁<x₂ : RelA x₁ x₂) → (x₁ , y₁) < (x₂ , y₂)
189190
right : ∀ {x y₁ y₂} (y₁<y₂ : RelB x y₁ y₂) → (x , y₁) < (x , y₂)

0 commit comments

Comments
 (0)