Documentation
Init
.
Data
.
Option
.
BasicAux
Search
return to top
source
Imports
Init.Util
Init.Data.Option.Basic
Imported by
Init.Data.Option.Lemmas
Init.Data.Option
Init.Meta
Option
.
get!
source
@[inline]
def
Option
.
get!
{
α
:
Type
u}
[
Inhabited
α
]
:
Option
α
→
α
Extracts the value from an
Option
, panicking on
none
.
Equations
(
some
x_1
)
.
get!
=
x_1
none
.
get!
=
panicWithPosWithDecl
"Init.Data.Option.BasicAux"
"Option.get!"
19
14
"value is none"