Documentation
Lean
.
Data
.
LOption
Search
Google site search
Lean
.
Data
.
LOption
source
Imports
Init
Imported by
Lean
.
LOption
Lean
.
instInhabitedLOption
Lean
.
instBEqLOption
Lean
.
instToStringLOption
Option
.
toLOption
toLOptionM
source
inductive
Lean
.
LOption
(α :
Type
u)
:
Type
u
none:
{
α
:
Type
u} →
Lean.LOption
α
some:
{
α
:
Type
u} →
α
→
Lean.LOption
α
undef:
{
α
:
Type
u} →
Lean.LOption
α
Instances For
source
instance
Lean
.
instInhabitedLOption
:
{
a
:
Type
u_1} →
Inhabited
(
Lean.LOption
a
)
source
instance
Lean
.
instBEqLOption
:
{
α
:
Type
u_1} →
[
inst
:
BEq
α
] →
BEq
(
Lean.LOption
α
)
source
instance
Lean
.
instToStringLOption
{α :
Type
u_1}
[
ToString
α
]
:
ToString
(
Lean.LOption
α
)
source
def
Option
.
toLOption
{α :
Type
u}
:
Option
α
→
Lean.LOption
α
Instances For
source
@[inline]
def
toLOptionM
{α :
Type
}
{m :
Type
→
Type
}
[
Monad
m
]
(x :
m
(
Option
α
)
)
:
m
(
Lean.LOption
α
)
Instances For