We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent df6fcac commit 928d3eeCopy full SHA for 928d3ee
1 file changed
src/Data/Rational/Unnormalised/Properties.agda
@@ -1974,7 +1974,7 @@ Please use *-monoʳ-≤-nonNeg instead."
1974
*-monoˡ-≤-pos : ∀ {r} → Positive r → (_* r) Preserves _≤_ ⟶ _≤_
1975
*-monoˡ-≤-pos r@{mkℚᵘ +[1+ _ ] _} _ = *-monoˡ-≤-nonNeg r
1976
{-# WARNING_ON_USAGE *-monoˡ-≤-pos
1977
-"Warning: *-monoˡ-≤-nonNeg was deprecated in v2.0.
+"Warning: *-monoˡ-≤-pos was deprecated in v2.0.
1978
Please use *-monoˡ-≤-nonNeg instead."
1979
#-}
1980
≤-steps = p≤q⇒p≤r+q
0 commit comments