Docstring for Int.mod is misleading #5204
Labels
bug
Something isn't working
documentation
Documentation improvement
P-high
We will work on this issue
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
The docstring for
Int.mod
(permalink) contains some nice examples which document the behavior of the%
operator. Unfortunately,%
onInt
is actuallyInt.emod
, and so the examples actually explain a different function.Steps to Reproduce
Expected behavior: Docstring documents the function
Actual behavior: Docstring documents a different function.
Versions
e1cbae2
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: