NonemptyList

Stream: Is there code for X?

[Scott Morrison]

Do we have API for nonempty lists sitting around somewhere that I am not seeing?

I wanted to compute the minimum of a list that I know is nonempty, and had to write:

import Mathlib.Data.List.MinMax

theorem List.minimum_ne_top_of_length_pos [LinearOrder α]
    {L : List α} (h : 0 < L.length) : L.minimum ≠ ⊤ :=
  match L, h with
  | _ :: _, _ => by simp [List.minimum_cons]

def List.minimum_length_pos [LinearOrder α] {L : List α} (h : 0 < L.length) : α :=
  WithTop.untop L.minimum (List.minimum_ne_top_of_length_pos h)

Surely someone has needed this previously? Possibly even with a bundled NonemptyList?

[Scott Morrison]

(One might wonder whether such a NonemptyList should be defined via L ≠ [] or 0 < L.length. My vote would be for the later.)

[Yury G. Kudryashov]

Scott Morrison said:

(One might wonder whether such a NonemptyList should be defined via L ≠ [] or 0 < L.length. My vote would be for the later.)

Why not as in std4#16 (hd : α) (tl : List α)?

[Yury G. Kudryashov]

We have docs#List.minimum_eq_none

[Yury G. Kudryashov]

(should be rewritten as minimum_eq_top)

[Pol'tta / Miyahara Kō]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Free.html#FreeSemigroup