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