Init.Data.Option.BasicAux

{α : Type u} [Inhabited α] : Option α → α

Full source

/--
Extracts the value from an `Option`, panicking on `none`.
-/
@[inline] def get! {α : Type u} [Inhabited α] : Option α → α
  | some x => x
  | none   => panic! "value is none"

Extract value from `Option` with panic on `none`

Informal description

Given an optional value of type `Option α` and a default value of type `α` (ensured by the `Inhabited` instance), this function extracts the value if it is `some x`, and panics with the message "value is none" if the input is `none`.