Zulip Chat Archive
Stream: Is there code for X?
Topic: Unwrapping Option
Alex Keizer (Jul 18 2023 at 13:09):
Does the following exists already?
def Option.unwrap (opt : Option α) (is_some : opt.isSome) : α :=
match opt with
| some a => a
| none => False.elim <| by simp at is_some
Kyle Miller (Jul 18 2023 at 13:18):
Last updated: Dec 20 2023 at 11:08 UTC