wrong docstring for integer division?

Stream: lean4

[David Loeffler]

If I type a / sign in VSCode and hover over it, a docstring pops up saying:

a / b computes the result of dividing a by b. The meaning of this notation is type-dependent. [...] For Nat and Int, a / b rounds toward 0.

However, the statement about rounding for Int doesn't seem to be true, because #eval (-1 / 2 : ℤ) returns -1, not 0. The offending docstring seems to be class HDiv in Init.Prelude.

[Kim Morrison]

Good catch! The behaviour changed recently. (It has long been overriden in Std.)

[Kim Morrison]

@David Loeffler, would you check lean#3734 for me?