LawfulTraversable instances #
This file provides instances of LawfulTraversable
for types from the core library: Option
,
List
and Sum
.
theorem
Option.comp_traverse
{F G : Type u → Type u}
[Applicative F]
[Applicative G]
[LawfulApplicative G]
{α : Type u_1}
{β γ : Type u}
(f : β → F γ)
(g : α → G β)
(x : Option α)
:
theorem
Option.naturality
{F G : Type u → Type u}
[Applicative F]
[Applicative G]
[LawfulApplicative G]
(η : ApplicativeTransformation F G)
[LawfulApplicative F]
{α : Type u_1}
{β : Type u}
(f : α → F β)
(x : Option α)
:
theorem
List.comp_traverse
{F G : Type u → Type u}
[Applicative F]
[Applicative G]
[LawfulApplicative G]
{α : Type u_1}
{β γ : Type u}
(f : β → F γ)
(g : α → G β)
(x : List α)
:
theorem
List.naturality
{F G : Type u → Type u}
[Applicative F]
[Applicative G]
[LawfulApplicative G]
[LawfulApplicative F]
(η : ApplicativeTransformation F G)
{α : Type u_1}
{β : Type u}
(f : α → F β)
(x : List α)
:
@[simp]
@[simp]
theorem
List.traverse_cons
{F : Type u → Type u}
[Applicative F]
{α' β' : Type u}
(f : α' → F β')
(a : α')
(l : List α')
:
@[simp]
theorem
List.traverse_append
{F : Type u → Type u}
[Applicative F]
{α' β' : Type u}
(f : α' → F β')
[LawfulApplicative F]
(as bs : List α')
:
theorem
Sum.traverse_map
{σ : Type u}
{G : Type u → Type u}
[Applicative G]
{α β γ : Type u}
(g : α → β)
(f : β → G γ)
(x : σ ⊕ α)
:
theorem
Sum.map_traverse
{σ : Type u}
{G : Type u → Type u}
[Applicative G]
[LawfulApplicative G]
{α : Type u_1}
{β γ : Type u}
(g : α → G β)
(f : β → γ)
(x : σ ⊕ α)
:
theorem
Sum.naturality
{σ : Type u}
{F G : Type u → Type u}
[Applicative F]
[Applicative G]
[LawfulApplicative G]
[LawfulApplicative F]
(η : ApplicativeTransformation F G)
{α : Type u_1}
{β : Type u}
(f : α → F β)
(x : σ ⊕ α)
: