Documentation
Init.Data.Option.BasicAux
Google site search
Init.Data.Option.BasicAux
source
Imports
Init.Util
Init.Data.Option.Basic
Imported by
Option.get!
source
@[inline]
def
Option.get!
{α :
Type
u}
[inst :
Inhabited
α
]
:
Option
α
→
α
Equations
Option.get!
x
=
match
x
with |
some
x
=>
x
|
none
=>
panicWithPosWithDecl
"Init.Data.Option.BasicAux"
"Option.get!"
16
14
"value is none"