Documentation
Mathlib
.
Control
.
Lawful
Search
return to top
source
Imports
Init
Mathlib.Tactic.Basic
Imported by
StateT
.
mk
StateT
.
run_mk
ExceptT
.
run_monadLift
ExceptT
.
run_monadMap
ReaderT
.
mk
ReaderT
.
run_mk
Functor Laws, applicative laws, and monad Laws
#
source
def
StateT
.
mk
{
σ
:
Type
u}
{
m
:
Type
u →
Type
v
}
{
α
:
Type
u}
(
f
:
σ
→
m
(
α
×
σ
)
)
:
StateT
σ
m
α
Equations
StateT.mk
f
=
f
Instances For
source
@[simp]
theorem
StateT
.
run_mk
{
σ
:
Type
u}
{
m
:
Type
u →
Type
v
}
{
α
:
Type
u}
(
f
:
σ
→
m
(
α
×
σ
)
)
(
st
:
σ
)
:
(
StateT.mk
f
)
.
run
st
=
f
st
source
@[simp]
theorem
ExceptT
.
run_monadLift
{
α
ε
:
Type
u}
{
m
:
Type
u →
Type
v
}
{
n
:
Type
u →
Type
u_1
}
[
Monad
m
]
[
MonadLiftT
n
m
]
(
x
:
n
α
)
:
(
monadLift
x
)
.
run
=
Except.ok
<$>
monadLift
x
source
@[simp]
theorem
ExceptT
.
run_monadMap
{
α
ε
:
Type
u}
{
m
:
Type
u →
Type
v
}
(
x
:
ExceptT
ε
m
α
)
{
n
:
Type
u →
Type
u_1
}
[
MonadFunctorT
n
m
]
(
f
:
{
α
:
Type
u} →
n
α
→
n
α
)
:
(
monadMap
f
x
)
.
run
=
monadMap
f
x
.
run
source
def
ReaderT
.
mk
{
m
:
Type
u →
Type
v
}
{
α
σ
:
Type
u}
(
f
:
σ
→
m
α
)
:
ReaderT
σ
m
α
Equations
ReaderT.mk
f
=
f
Instances For
source
@[simp]
theorem
ReaderT
.
run_mk
{
m
:
Type
u →
Type
v
}
{
α
σ
:
Type
u}
(
f
:
σ
→
m
α
)
(
r
:
σ
)
:
(
ReaderT.mk
f
)
.
run
r
=
f
r