Zulip Chat Archive

Stream: Is there code for X?

Topic: head of a list?


view this post on Zulip Kevin Lacker (Oct 02 2020 at 20:57):

Is there a method for "the head of a list"? Like to express the proposition, "the first element of the list L is 6."

view this post on Zulip Kenny Lau (Oct 02 2020 at 20:59):

list.head

view this post on Zulip Kevin Lacker (Oct 02 2020 at 21:00):

ehhh ok thanks. now i wonder why i couldn't find that

view this post on Zulip Kevin Lacker (Oct 02 2020 at 21:00):

i guess i was stumped because it is not near the definition of list. well, thanks!

view this post on Zulip Jalex Stark (Oct 04 2020 at 12:22):

There's a search bar on the mathlib_docs page. Maybe this works to take you there docs#list.head ?

view this post on Zulip Gabriel Ebner (Oct 05 2020 at 08:00):

Is there a method for "the head of a list"?

Surprisingly, also docs#the.head.of.a.list takes you to the right definition.


Last updated: May 17 2021 at 14:12 UTC