Zulip Chat Archive
Stream: new members
Topic: Array.head?
Asei Inoue (Oct 19 2025 at 13:55):
we don't have Array.head? ?
def Array.head? (arr : Array α) : Option α :=
match arr with
| ⟨[]⟩ => none
| ⟨x :: _⟩ => some x
Asei Inoue (Oct 19 2025 at 14:03):
self resolved
Eric Wieser (Oct 19 2025 at 14:04):
arr[0]??
Asei Inoue (Oct 19 2025 at 14:04):
yes.
Last updated: Dec 20 2025 at 21:32 UTC