Skip to content

Commit 2433c3c

Browse files
committed
fix: deprecated names from agda#2206 / agda#2168
1 parent 6eab5f2 commit 2433c3c

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/Data/Rational/Unnormalised/Properties.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -1144,7 +1144,7 @@ p≤q⇒0≤q-p {p} {q} p≤q = begin
11441144
*-zeroˡ p@record{} = *≡* refl
11451145

11461146
*-zeroʳ : RightZero _≃_ 0ℚᵘ _*_
1147-
*-zeroʳ = Consequences.comm+zeˡ⇒zeʳ ≃-setoid *-comm *-zeroˡ
1147+
*-zeroʳ = Consequences.commzeˡ⇒zeʳ ≃-setoid *-comm *-zeroˡ
11481148

11491149
*-zero : Zero _≃_ 0ℚᵘ _*_
11501150
*-zero = *-zeroˡ , *-zeroʳ
@@ -1171,7 +1171,7 @@ invertible⇒≄ {p} {q} (1/p-q , 1/x*x≃1 , x*1/x≃1) p≃q = 0≄1 (begin
11711171
in *≡* eq where open ℤ-solver
11721172

11731173
*-distribʳ-+ : _DistributesOverʳ_ _≃_ _*_ _+_
1174-
*-distribʳ-+ = Consequences.comm+distrˡ⇒distrʳ ≃-setoid +-cong *-comm *-distribˡ-+
1174+
*-distribʳ-+ = Consequences.commdistrˡ⇒distrʳ ≃-setoid +-cong *-comm *-distribˡ-+
11751175

11761176
*-distrib-+ : _DistributesOver_ _≃_ _*_ _+_
11771177
*-distrib-+ = *-distribˡ-+ , *-distribʳ-+

0 commit comments

Comments
 (0)