Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit a4fbbc6

Browse files
committedDec 28, 2023
leftover from agda#2182: subtle naming 'bug'/anomaly
1 parent 618a6a9 commit a4fbbc6

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed
 

‎src/Data/Nat/Divisibility.agda

+4-4
Original file line numberDiff line numberDiff line change
@@ -349,12 +349,12 @@ hasNonTrivialDivisor-≢ d≢n d∣n
349349

350350
hasNonTrivialDivisor-∣ : m HasNonTrivialDivisorLessThan n m ∣ o
351351
o HasNonTrivialDivisorLessThan n
352-
hasNonTrivialDivisor-∣ (hasNonTrivialDivisor d<n d∣m) n∣o
353-
= hasNonTrivialDivisor d<n (∣-trans d∣m n∣o)
352+
hasNonTrivialDivisor-∣ (hasNonTrivialDivisor d<n d∣m) m∣o
353+
= hasNonTrivialDivisor d<n (∣-trans d∣m m∣o)
354354

355355
-- Monotonicity wrt ≤
356356

357357
hasNonTrivialDivisor-≤ : m HasNonTrivialDivisorLessThan n n ≤ o
358358
m HasNonTrivialDivisorLessThan o
359-
hasNonTrivialDivisor-≤ (hasNonTrivialDivisor d<n d∣m) m≤o
360-
= hasNonTrivialDivisor (<-≤-trans d<n m≤o) d∣m
359+
hasNonTrivialDivisor-≤ (hasNonTrivialDivisor d<n d∣m) n≤o
360+
= hasNonTrivialDivisor (<-≤-trans d<n n≤o) d∣m

0 commit comments

Comments
 (0)
Please sign in to comment.