Zulip Chat Archive

Stream: general

Topic: nth_le


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

@[simp] def nth_le : Π (l : list α) (n), n < l.length  α
| []       n     h := absurd h (not_lt_zero n)
| (a :: l) 0     h := a
| (a :: l) (n+1) h := nth_le l n (le_of_succ_le_succ h)

So why exactly is this called nth_le?


Last updated: May 14 2021 at 07:19 UTC