Skip to content

Commit ec4c543

Browse files
committed
fix whitespace
1 parent 5062d3e commit ec4c543

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Data/Rational/Properties.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -316,7 +316,7 @@ normalize-injective-≃ m n c d eq = ℕ./-cancelʳ-≡
316316
(m ℕ./ gcd[m,c]) ℕ.* (d ℕ./ gcd[n,d]) ≡⟨ cong₂ ℕ._*_ m/gcd[m,c]≡n/gcd[n,d] (sym c/gcd[m,c]≡d/gcd[n,d]) ⟩
317317
(n ℕ./ gcd[n,d]) ℕ.* (c ℕ./ gcd[m,c]) ≡⟨ ℕ./-*-interchange gcd[n,d]∣n gcd[m,c]∣c ⟨
318318
(n ℕ.* c) ℕ./ (gcd[n,d] ℕ.* gcd[m,c]) ≡⟨ ℕ./-congʳ (ℕ.*-comm gcd[n,d] gcd[m,c]) ⟩
319-
(n ℕ.* c) ℕ./ (gcd[m,c] ℕ.* gcd[n,d]) ∎
319+
(n ℕ.* c) ℕ./ (gcd[m,c] ℕ.* gcd[n,d]) ∎
320320
where
321321
open ≡-Reasoning
322322
gcd[m,c] = ℕ.gcd m c

0 commit comments

Comments
 (0)