We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
2 parents 018dd40 + 992f6b7 commit 8483681Copy full SHA for 8483681
src/Data/Nat/GCD.agda
@@ -33,7 +33,7 @@ import Relation.Nullary.Decidable as Dec
33
-- Calculated via Euclid's algorithm. In order to show progress,
34
-- avoiding the initial step where the first argument may increase, it
35
-- is necessary to first define a version `gcd′` which assumes that the
36
--- first argument is strictly smaller than the second. The full `gcd`
+-- second argument is strictly smaller than the first. The full `gcd`
37
-- function then compares the two arguments and applies `gcd′`
38
-- accordingly.
39
0 commit comments