where is `List.max!`

Stream: Is there code for X?

[Asei Inoue]

I can't find where List.max! is defined for List.max?. Is there a corresponding function for this?

[Kim Morrison]

I don't think so. Are you expecting it to panic?

There is List.maximum defined in Mathlib that returns a WithTop.

[Asei Inoue]

yes, panic is expected.
PR adding this is welcome?

[Kim Morrison]

Perhaps at Batteries or Mathlib; not lean4 for now, please.

[Asei Inoue]

done! https://github.com/leanprover-community/batteries/pull/1174