From 8af25455aea4084ce14ffa2ae505ce0cb9dfe3ca Mon Sep 17 00:00:00 2001 From: Marcus Rossel Date: Wed, 9 Aug 2023 12:11:29 +0200 Subject: [PATCH] doc: fix comment for `Nat.sub` --- src/Init/Prelude.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index fcf7b02636..4e2c2b9f8e 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1706,7 +1706,7 @@ instance : Min Nat := minOfLe set_option bootstrap.genMatcherCode false in /-- (Truncated) subtraction of natural numbers. Because natural numbers are not -closed under subtraction, we define `m - n` to be `0` when `n < m`. +closed under subtraction, we define `n - m` to be `0` when `n < m`. This definition is overridden in both the kernel and the compiler to efficiently evaluate using the "bignum" representation (see `Nat`). The definition provided