Zulip Chat Archive

Stream: general

Topic: inconsistency of theorem naming


view this post on Zulip Kenny Lau (Jul 27 2018 at 07:05):

#check list.index_of_nth_le _
/-
list.nth_le ?M_4 (list.index_of ?M_3 ?M_4) ?M_5 = ?M_3
-/
#check list.nth_le_index_of _ _ _
/-
list.index_of (list.nth_le ?M_3 ?M_5 ?M_6) ?M_3 = ?M_5
-/
#check list.nth_le_of_fn _ _
/-
list.nth_le (list.of_fn ?M_3) (?M_4.val) _ = ?M_3 ?M_4
-/

view this post on Zulip Kenny Lau (Jul 27 2018 at 07:05):

all three examples consist of a function followed by another function in the name

view this post on Zulip Kenny Lau (Jul 27 2018 at 07:06):

in the last example, the actual order in the statement is the same as the order in the name, i.e. nth_le and then of_fn

view this post on Zulip Kenny Lau (Jul 27 2018 at 07:06):

but in the first two examples, the order is swapped


Last updated: May 08 2021 at 19:11 UTC