swap! docstring seems wrong

Stream: lean4

[Wrenna Robson]

This technically relates to a mathlib4 thing but it feels sufficently close to being relevant outside it that I am asking in this stream.
Reading the docstring for
Array.swap!, it claims that when the inputs are outside the length, there is a panic. But that certainly isn't true for the implementation within Lean, and it doesn't seem to be true for the external implementation lean_array_swap either.

Here is the relevant code:

static inline lean_object * lean_array_swap(lean_obj_arg a, b_lean_obj_arg i, b_lean_obj_arg j) {
    if (!lean_is_scalar(i) || !lean_is_scalar(j)) return a;
    size_t ui = lean_unbox(i);
    size_t uj = lean_unbox(j);
    size_t sz = lean_to_array(a)->m_size;
    if (ui >= sz || uj >= sz) return a;
    return lean_array_uswap(a, ui, uj);
}

This really appears to not panic when they are out of bounds, but instead simply just doesn't change the Array. This is in contrast to, say, docs#Array.get!, which does panic there I think.

This suggests to me that a) Array.swap! is misnamed (! implies a possibility of panic, to me), b) we probably need only one of Array.swapN and Array.swap! (probably the latter).

[Kim Morrison]

Doc-string corrected in lean#4869. I'll consider the naming again soon.

[Wrenna Robson]

Thanks.

[Joachim Breitner]

My bad, should have updated the docstring in https://github.com/leanprover/lean4/pull/3197

[Wrenna Robson]

https://leanprover-community.github.io/mathlib4_docs/Init/Data/Vector/Basic.html#Vector.swapIfInBounds

This also has the (incorrect) docstring.

[Wrenna Robson]

@Kim Morrison FYI