HepLean Documentation
Init
.
Data
.
Option
.
BasicAux
Search
Google site search
return to top
source
Imports
Init.Util
Init.Data.Option.Basic
Imported by
Option
.
get!
source
@[inline]
def
Option
.
get!
{α :
Type
u}
[
Inhabited
α
]
:
Option
α
→
α
Equations
(
some
x_1
)
.get!
=
x_1
none
.get!
=
panicWithPosWithDecl
"Init.Data.Option.BasicAux"
"Option.get!"
16
14
"value is none"
Instances For