Getting the first element of a nonempty list

Stream: Is there code for X?

[Anne Baanen]

I have a list xs and an element x ∈ xs. What is the best way to get the first element of xs: create a local inhabited instance and use docs#list.head, use docs#list.head' and prove it returns some, or something else?

[Anne Baanen]

In other words, does the following already exist:

def list.head_of_mem {α : Type*} : Π (xs : list α) {x : α} (h : x ∈ xs), α
| (y :: _) _ _ := y

[Pontus Sundqvist]

You can use list.exists_cons_of_ne_nil to get it.

theorem get_head (x : ℕ) (l : list ℕ) (hx : x ∈ l) :
  ∃ (b : ℕ) (L : list ℕ), l = b :: L :=
list.exists_cons_of_ne_nil (list.ne_nil_of_mem hx)

[Anne Baanen]

Unfortunately, that would make the definition noncomputable. :(

[Ruben Van de Velde]

Oddly, list.last does exist in that shape

[Yakov Pechersky]

I use list.nth_le 0 (length_pos proof based on the fact that there is an element in it)