Unwrapping Option

Stream: Is there code for X?

[Alex Keizer]

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]

docs#Option.get