Skip to content

Commit

Permalink
fix: name of Int.tdiv in HDiv.hDiv docstring (#6885)
Browse files Browse the repository at this point in the history
This PR fixes the name of the truncating integer division function in
the `HDiv.hDiv` docstring (which is shown when hovering over `/`). It
was changed from `Int.div` to `Int.tdiv` in #5301.
  • Loading branch information
TwoFX authored Jan 31, 2025
1 parent 6c2573f commit fe3a78d
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Init/Prelude.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1222,7 +1222,7 @@ class HDiv (α : Type u) (β : Type v) (γ : outParam (Type w)) where
It is implemented as `Int.ediv`, the unique function satisfying
`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).
`Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
usually resulting in `inf` or `nan`. -/
hDiv : α → β → γ
Expand Down

0 comments on commit fe3a78d

Please sign in to comment.