Skip to content

Commit 07f1860

Browse files
Fix 2 incorrect deprecation warnings in Data.Nat.Properties (#1201)
1 parent a76aa80 commit 07f1860

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/Data/Nat/Properties.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2301,13 +2301,13 @@ Please use m∸n≤m instead (note, you will need to switch the argument order).
23012301

23022302
∀[m≤n⇒m≢o]⇒o<n : n o ( {m} m ≤ n m ≢ o) n < o
23032303
∀[m≤n⇒m≢o]⇒o<n = ∀[m≤n⇒m≢o]⇒n<o
2304-
{-# WARNING_ON_USAGE n∸m≤∣n-m∣
2304+
{-# WARNING_ON_USAGE ∀[m≤n⇒m≢o]⇒o<n
23052305
"Warning: ∀[m≤n⇒m≢o]⇒o<n was deprecated in v1.3.
23062306
Please use ∀[m≤n⇒m≢o]⇒n<o instead."
23072307
#-}
23082308
∀[m<n⇒m≢o]⇒o≤n : n o ( {m} m < n m ≢ o) n ≤ o
23092309
∀[m<n⇒m≢o]⇒o≤n = ∀[m<n⇒m≢o]⇒n≤o
2310-
{-# WARNING_ON_USAGE n∸m≤∣n-m∣
2310+
{-# WARNING_ON_USAGE ∀[m<n⇒m≢o]⇒o≤n
23112311
"Warning: ∀[m<n⇒m≢o]⇒o≤n was deprecated in v1.3.
23122312
Please use ∀[m<n⇒m≢o]⇒n≤o instead."
23132313
#-}

0 commit comments

Comments
 (0)