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

doc: fix HDiv and HMod doc-strings (#3734)

Browse source 
As reported by @loefflerd on
[zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/wrong.20docstring.20for.20integer.20division.3F/near/428076692).
This commit is contained in:
Scott Morrison 2024-03-22 10:46:41 +11:00 • committed by GitHub
parent 966fa800f8
commit 67c7729f96
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Init/Prelude.lean
View file

@ -1194,7 +1194,12 @@ class HDiv (α : Type u) (β : Type v) (γ : outParam (Type w)) where
/-- `a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat` and `Int`, `a / b` rounds toward 0.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
It is implemented as `Int.ediv`, the unique function satisfiying
`a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
Other rounding conventions are available using the functions
`Int.fdiv` (floor rounding) and `Int.div` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
usually resulting in `inf` or `nan`. -/
hDiv : α → β → γ
@ -1206,7 +1211,8 @@ This enables the notation `a % b : γ` where `a : α`, `b : β`.
class HMod (α : Type u) (β : Type v) (γ : outParam (Type w)) where
/-- `a % b` computes the remainder upon dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For `Nat` and `Int`, `a % 0` is defined to be `a`. -/
* For `Nat` and `Int` it satisfies `a % b + b * (a / b) = a`,
and `a % 0` is defined to be `a`. -/
hMod : α → β → γ
/--