Zulip Chat Archive

Stream: Is there code for X?

Topic: list.nth is either none


view this post on Zulip Marcus Rossel (Feb 16 2021 at 19:10):

I'm not sure if this is two specific, but is there some lemma in the direction of?:

example {α : Type*} (l : list (option α)) (n : ) :
  (l.nth n).join = none  (l.nth n = (some none)  l.nth n = none)

Thanks

view this post on Zulip Floris van Doorn (Feb 16 2021 at 19:16):

If you generalize l.nth n to an arbitary element of option (option α), this should be added to mathlib as option.join_eq_none. Contrast docs#option.join_ne_none

view this post on Zulip Floris van Doorn (Feb 16 2021 at 19:24):

import data.option.basic

namespace option

lemma join_eq_none {α : Type*} (o : option (option α)) : o.join = none  o = none  o = some none :=
by rcases o with _|_|_; simp

end option

view this post on Zulip Floris van Doorn (Feb 16 2021 at 19:29):

#6269

view this post on Zulip Marcus Rossel (Feb 16 2021 at 19:29):

This community is just so awesome :blush:
Thanks!


Last updated: May 07 2021 at 22:14 UTC