max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix comment for Nat.sub

Browse source
This commit is contained in:
Marcus Rossel 2023-08-09 12:11:29 +02:00 • committed by Leonardo de Moura
parent befc4b997b
commit 8af25455ae
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Prelude.lean
View file

@ -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