Free constructions
Main definitions
free_magma α: free magma (structure with binary operation without any axioms) over alphabetα, defined inductively, with traversable instance and decidable equality.magma.free_semigroup α: free semigroup over magmaα.free_semigroup α: free semigroup over alphabetα, defined as a synonym forα × list α(i.e. nonempty lists), with traversable instance and decidable equality.free_semigroup_free_magma α: isomorphism betweenmagma.free_semigroup (free_magma α)andfree_semigroup α.
- of : Π (α : Type u), α → free_magma α
- mul : Π (α : Type u), free_magma α → free_magma α → free_magma α
Free magma over a given alphabet.
@[instance]
@[instance]
- of : Π (α : Type u), α → free_add_magma α
- add : Π (α : Type u), free_add_magma α → free_add_magma α → free_add_magma α
Free nonabelian additive magma over a given alphabet.
@[instance]
Equations
@[instance]
@[instance]
Equations
@[simp]
def
free_magma.rec_on'
{α : Type u}
{C : free_magma α → Sort l}
(x : free_magma α) :
(Π (x : α), C (free_magma.of x)) → (Π (x y : free_magma α), C x → C y → C (x * y)) → C x
Recursor for free_magma using x * y instead of free_magma.mul x y.
def
free_add_magma.rec_on'
{α : Type u}
{C : free_add_magma α → Sort l}
(x : free_add_magma α) :
(Π (x : α), C (free_add_magma.of x)) → (Π (x y : free_add_magma α), C x → C y → C (x + y)) → C x
Recursor for free_add_magma using x + y instead of free_add_magma.add x y.
Lifts a function α → β to a magma homomorphism free_magma α → β given a magma β.
Equations
- free_magma.lift f (x * y) = free_magma.lift f x * free_magma.lift f y
- free_magma.lift f (free_magma.of x) = f x
Lifts a function α → β to an additive magma homomorphism free_add_magma α → β given
an additive magma β.
Equations
- free_add_magma.lift f (x + y) = free_add_magma.lift f x + free_add_magma.lift f y
- free_add_magma.lift f (free_add_magma.of x) = f x
@[simp]
theorem
free_magma.lift_of
{α : Type u}
{β : Type v}
[has_mul β]
(f : α → β)
(x : α) :
free_magma.lift f (free_magma.of x) = f x
@[simp]
theorem
free_add_magma.lift_of
{α : Type u}
{β : Type v}
[has_add β]
(f : α → β)
(x : α) :
free_add_magma.lift f (free_add_magma.of x) = f x
@[simp]
theorem
free_magma.lift_mul
{α : Type u}
{β : Type v}
[has_mul β]
(f : α → β)
(x y : free_magma α) :
free_magma.lift f (x * y) = free_magma.lift f x * free_magma.lift f y
@[simp]
theorem
free_add_magma.lift_add
{α : Type u}
{β : Type v}
[has_add β]
(f : α → β)
(x y : free_add_magma α) :
free_add_magma.lift f (x + y) = free_add_magma.lift f x + free_add_magma.lift f y
theorem
free_magma.lift_unique
{α : Type u}
{β : Type v}
[has_mul β]
(f : free_magma α → β) :
(∀ (x y : free_magma α), f (x * y) = f x * f y) → f = free_magma.lift (f ∘ free_magma.of)
theorem
free_add_magma.lift_unique
{α : Type u}
{β : Type v}
[has_add β]
(f : free_add_magma α → β) :
(∀ (x y : free_add_magma α), f (x + y) = f x + f y) → f = free_add_magma.lift (f ∘ free_add_magma.of)
The unique magma homomorphism free_magma α → free_magma β that sends
each of x to of (f x).
Equations
- free_magma.map f (x * y) = free_magma.map f x * free_magma.map f y
- free_magma.map f (free_magma.of x) = free_magma.of (f x)
The unique additive magma homomorphism free_add_magma α → free_add_magma β that sends
each of x to of (f x).
Equations
- free_add_magma.map f (x + y) = free_add_magma.map f x + free_add_magma.map f y
- free_add_magma.map f (free_add_magma.of x) = free_add_magma.of (f x)
@[simp]
theorem
free_add_magma.map_of
{α : Type u}
{β : Type v}
(f : α → β)
(x : α) :
free_add_magma.map f (free_add_magma.of x) = free_add_magma.of (f x)
@[simp]
theorem
free_magma.map_of
{α : Type u}
{β : Type v}
(f : α → β)
(x : α) :
free_magma.map f (free_magma.of x) = free_magma.of (f x)
@[simp]
theorem
free_add_magma.map_add
{α : Type u}
{β : Type v}
(f : α → β)
(x y : free_add_magma α) :
free_add_magma.map f (x + y) = free_add_magma.map f x + free_add_magma.map f y
@[simp]
theorem
free_magma.map_mul
{α : Type u}
{β : Type v}
(f : α → β)
(x y : free_magma α) :
free_magma.map f (x * y) = free_magma.map f x * free_magma.map f y
def
free_magma.rec_on''
{α : Type u}
{C : free_magma α → Sort l}
(x : free_magma α) :
(Π (x : α), C (has_pure.pure x)) → (Π (x y : free_magma α), C x → C y → C (x * y)) → C x
Recursor on free_magma using pure instead of of.
def
free_add_magma.rec_on''
{α : Type u}
{C : free_add_magma α → Sort l}
(x : free_add_magma α) :
(Π (x : α), C (has_pure.pure x)) → (Π (x y : free_add_magma α), C x → C y → C (x + y)) → C x
Recursor on free_add_magma using pure instead of of.
@[simp]
theorem
free_add_magma.map_pure
{α β : Type u}
(f : α → β)
(x : α) :
f <$> has_pure.pure x = has_pure.pure (f x)
@[simp]
theorem
free_magma.map_pure
{α β : Type u}
(f : α → β)
(x : α) :
f <$> has_pure.pure x = has_pure.pure (f x)
@[simp]
@[simp]
@[simp]
theorem
free_add_magma.pure_bind
{α β : Type u}
(f : α → free_add_magma β)
(x : α) :
has_pure.pure x >>= f = f x
@[simp]
theorem
free_magma.pure_bind
{α β : Type u}
(f : α → free_magma β)
(x : α) :
has_pure.pure x >>= f = f x
@[simp]
theorem
free_add_magma.add_bind
{α β : Type u}
(f : α → free_add_magma β)
(x y : free_add_magma α) :
@[simp]
@[simp]
theorem
free_magma.pure_seq
{α β : Type u}
{f : α → β}
{x : free_magma α} :
has_pure.pure f <*> x = f <$> x
@[simp]
theorem
free_add_magma.pure_seq
{α β : Type u}
{f : α → β}
{x : free_add_magma α} :
has_pure.pure f <*> x = f <$> x
@[simp]
theorem
free_add_magma.add_seq
{α β : Type u}
{f g : free_add_magma (α → β)}
{x : free_add_magma α} :
@[simp]
@[instance]
Equations
def
free_magma.traverse
{m : Type u → Type u}
[applicative m]
{α β : Type u} :
(α → m β) → free_magma α → m (free_magma β)
free_magma is traversable.
Equations
- free_magma.traverse F (x * y) = has_mul.mul <$> free_magma.traverse F x <*> free_magma.traverse F y
- free_magma.traverse F (free_magma.of x) = free_magma.of <$> F x
def
free_add_magma.traverse
{m : Type u → Type u}
[applicative m]
{α β : Type u} :
(α → m β) → free_add_magma α → m (free_add_magma β)
free_add_magma is traversable.
Equations
- free_add_magma.traverse F (x + y) = has_add.add <$> free_add_magma.traverse F x <*> free_add_magma.traverse F y
- free_add_magma.traverse F (free_add_magma.of x) = free_add_magma.of <$> F x
@[instance]
@[simp]
theorem
free_add_magma.traverse_pure
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
(x : α) :
traversable.traverse F (has_pure.pure x) = has_pure.pure <$> F x
@[simp]
theorem
free_magma.traverse_pure
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
(x : α) :
traversable.traverse F (has_pure.pure x) = has_pure.pure <$> F x
@[simp]
theorem
free_magma.traverse_pure'
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β) :
traversable.traverse F ∘ has_pure.pure = λ (x : α), has_pure.pure <$> F x
@[simp]
theorem
free_add_magma.traverse_pure'
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β) :
traversable.traverse F ∘ has_pure.pure = λ (x : α), has_pure.pure <$> F x
@[simp]
theorem
free_add_magma.traverse_add
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
(x y : free_add_magma α) :
traversable.traverse F (x + y) = has_add.add <$> traversable.traverse F x <*> traversable.traverse F y
@[simp]
theorem
free_magma.traverse_mul
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
(x y : free_magma α) :
traversable.traverse F (x * y) = has_mul.mul <$> traversable.traverse F x <*> traversable.traverse F y
@[simp]
theorem
free_add_magma.traverse_add'
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β) :
function.comp (traversable.traverse F) ∘ has_add.add = λ (x y : free_add_magma α), has_add.add <$> traversable.traverse F x <*> traversable.traverse F y
@[simp]
theorem
free_magma.traverse_mul'
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β) :
function.comp (traversable.traverse F) ∘ has_mul.mul = λ (x y : free_magma α), has_mul.mul <$> traversable.traverse F x <*> traversable.traverse F y
@[simp]
theorem
free_magma.traverse_eq
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
(x : free_magma α) :
free_magma.traverse F x = traversable.traverse F x
@[simp]
theorem
free_add_magma.traverse_eq
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
(x : free_add_magma α) :
@[simp]
@[simp]
theorem
free_add_magma.add_map_seq
{α : Type u}
(x y : free_add_magma α) :
has_add.add <$> x <*> y = x + y
@[instance]
Equations
- free_magma.is_lawful_traversable = {to_is_lawful_functor := free_magma.is_lawful_traversable._proof_1, id_traverse := free_magma.is_lawful_traversable._proof_2, comp_traverse := free_magma.is_lawful_traversable._proof_3, traverse_eq_map_id := free_magma.is_lawful_traversable._proof_4, naturality := free_magma.is_lawful_traversable._proof_5}
@[instance]
@[instance]
Equations
- free_magma.has_repr = {repr := free_magma.repr _inst_1}
Length of an element of a free magma.
Length of an element of a free additive magma.
Free additive semigroup over an additive magma.
Free semigroup over a magma.
Equations
- magma.free_semigroup α = quot (magma.free_semigroup.r α)
Embedding from additive magma to its free additive semigroup.
Embedding from magma to its free semigroup.
Equations
- magma.free_semigroup.of = quot.mk (magma.free_semigroup.r α)
@[instance]
theorem
magma.free_semigroup.induction_on
{α : Type u}
[has_mul α]
{C : magma.free_semigroup α → Prop}
(x : magma.free_semigroup α) :
(∀ (x : α), C (magma.free_semigroup.of x)) → C x
theorem
add_magma.free_add_semigroup.induction_on
{α : Type u}
[has_add α]
{C : add_magma.free_add_semigroup α → Prop}
(x : add_magma.free_add_semigroup α) :
(∀ (x : α), C (add_magma.free_add_semigroup.of x)) → C x
theorem
add_magma.free_add_semigroup.of_add_assoc
{α : Type u}
[has_add α]
(x y z : α) :
add_magma.free_add_semigroup.of (x + y + z) = add_magma.free_add_semigroup.of (x + (y + z))
theorem
magma.free_semigroup.of_mul_assoc
{α : Type u}
[has_mul α]
(x y z : α) :
magma.free_semigroup.of (x * y * z) = magma.free_semigroup.of (x * (y * z))
theorem
add_magma.free_add_semigroup.of_add_assoc_left
{α : Type u}
[has_add α]
(w x y z : α) :
add_magma.free_add_semigroup.of (w + (x + y + z)) = add_magma.free_add_semigroup.of (w + (x + (y + z)))
theorem
magma.free_semigroup.of_mul_assoc_left
{α : Type u}
[has_mul α]
(w x y z : α) :
magma.free_semigroup.of (w * (x * y * z)) = magma.free_semigroup.of (w * (x * (y * z)))
theorem
add_magma.free_add_semigroup.of_add_assoc_right
{α : Type u}
[has_add α]
(w x y z : α) :
add_magma.free_add_semigroup.of (w + x + y + z) = add_magma.free_add_semigroup.of (w + (x + y) + z)
theorem
magma.free_semigroup.of_mul_assoc_right
{α : Type u}
[has_mul α]
(w x y z : α) :
magma.free_semigroup.of (w * x * y * z) = magma.free_semigroup.of (w * (x * y) * z)
@[instance]
Equations
- magma.free_semigroup.semigroup = {mul := λ (x y : magma.free_semigroup α), quot.lift_on x (λ (p : α), quot.lift_on y (λ (q : α), quot.mk (magma.free_semigroup.r α) (p * q)) _) _, mul_assoc := _}
@[instance]
def
magma.free_semigroup.lift
{α : Type u}
[has_mul α]
{β : Type v}
[semigroup β]
(f : α → β) :
(∀ (x y : α), f (x * y) = f x * f y) → magma.free_semigroup α → β
Lifts a magma homomorphism α → β to a semigroup homomorphism magma.free_semigroup α → β
given a semigroup β.
Equations
- magma.free_semigroup.lift f hf = quot.lift f _
def
add_magma.free_add_semigroup.lift
{α : Type u}
[has_add α]
{β : Type v}
[add_semigroup β]
(f : α → β) :
(∀ (x y : α), f (x + y) = f x + f y) → add_magma.free_add_semigroup α → β
Lifts an additive magma homomorphism α → β to an additive semigroup homomorphism
add_magma.free_add_semigroup α → β given an additive semigroup β.
@[simp]
theorem
add_magma.free_add_semigroup.lift_of
{α : Type u}
[has_add α]
{β : Type v}
[add_semigroup β]
(f : α → β)
{hf : ∀ (x y : α), f (x + y) = f x + f y}
(x : α) :
@[simp]
theorem
magma.free_semigroup.lift_of
{α : Type u}
[has_mul α]
{β : Type v}
[semigroup β]
(f : α → β)
{hf : ∀ (x y : α), f (x * y) = f x * f y}
(x : α) :
magma.free_semigroup.lift f hf (magma.free_semigroup.of x) = f x
@[simp]
theorem
add_magma.free_add_semigroup.lift_add
{α : Type u}
[has_add α]
{β : Type v}
[add_semigroup β]
(f : α → β)
{hf : ∀ (x y : α), f (x + y) = f x + f y}
(x y : add_magma.free_add_semigroup α) :
add_magma.free_add_semigroup.lift f hf (x + y) = add_magma.free_add_semigroup.lift f hf x + add_magma.free_add_semigroup.lift f hf y
@[simp]
theorem
magma.free_semigroup.lift_mul
{α : Type u}
[has_mul α]
{β : Type v}
[semigroup β]
(f : α → β)
{hf : ∀ (x y : α), f (x * y) = f x * f y}
(x y : magma.free_semigroup α) :
magma.free_semigroup.lift f hf (x * y) = magma.free_semigroup.lift f hf x * magma.free_semigroup.lift f hf y
theorem
add_magma.free_add_semigroup.lift_unique
{α : Type u}
[has_add α]
{β : Type v}
[add_semigroup β]
(f : add_magma.free_add_semigroup α → β)
(hf : ∀ (x y : add_magma.free_add_semigroup α), f (x + y) = f x + f y) :
theorem
magma.free_semigroup.lift_unique
{α : Type u}
[has_mul α]
{β : Type v}
[semigroup β]
(f : magma.free_semigroup α → β)
(hf : ∀ (x y : magma.free_semigroup α), f (x * y) = f x * f y) :
def
magma.free_semigroup.map
{α : Type u}
[has_mul α]
{β : Type v}
[has_mul β]
(f : α → β) :
(∀ (x y : α), f (x * y) = f x * f y) → magma.free_semigroup α → magma.free_semigroup β
From a magma homomorphism α → β to a semigroup homomorphism
magma.free_semigroup α → magma.free_semigroup β.
Equations
def
add_magma.free_add_semigroup.map
{α : Type u}
[has_add α]
{β : Type v}
[has_add β]
(f : α → β) :
(∀ (x y : α), f (x + y) = f x + f y) → add_magma.free_add_semigroup α → add_magma.free_add_semigroup β
From an additive magma homomorphism α → β to an additive semigroup homomorphism
add_magma.free_add_semigroup α → add_magma.free_add_semigroup β.
@[simp]
theorem
magma.free_semigroup.map_of
{α : Type u}
[has_mul α]
{β : Type v}
[has_mul β]
(f : α → β)
{hf : ∀ (x y : α), f (x * y) = f x * f y}
(x : α) :
magma.free_semigroup.map f hf (magma.free_semigroup.of x) = magma.free_semigroup.of (f x)
@[simp]
theorem
magma.free_semigroup.map_mul
{α : Type u}
[has_mul α]
{β : Type v}
[has_mul β]
(f : α → β)
{hf : ∀ (x y : α), f (x * y) = f x * f y}
(x y : magma.free_semigroup α) :
magma.free_semigroup.map f hf (x * y) = magma.free_semigroup.map f hf x * magma.free_semigroup.map f hf y
@[simp]
theorem
add_magma.free_add_semigroup.map_add
{α : Type u}
[has_add α]
{β : Type v}
[has_add β]
(f : α → β)
{hf : ∀ (x y : α), f (x + y) = f x + f y}
(x y : add_magma.free_add_semigroup α) :
add_magma.free_add_semigroup.map f hf (x + y) = add_magma.free_add_semigroup.map f hf x + add_magma.free_add_semigroup.map f hf y
Free semigroup over a given alphabet. (Note: In this definition, the free semigroup does not contain the empty word.)
Equations
- free_semigroup α = (α × list α)
@[instance]
@[instance]
The embedding α → free_add_semigroup α.
The embedding α → free_semigroup α.
Equations
- free_semigroup.of x = (x, list.nil α)
@[instance]
@[instance]
Equations
def
free_add_semigroup.rec_on
{α : Type u}
{C : free_add_semigroup α → Sort l}
(x : free_add_semigroup α) :
(Π (x : α), C (free_add_semigroup.of x)) → (Π (x : α) (y : free_add_semigroup α), C (free_add_semigroup.of x) → C y → C (free_add_semigroup.of x + y)) → C x
Recursor for free additive semigroup using of and +.
def
free_semigroup.rec_on
{α : Type u}
{C : free_semigroup α → Sort l}
(x : free_semigroup α) :
(Π (x : α), C (free_semigroup.of x)) → (Π (x : α) (y : free_semigroup α), C (free_semigroup.of x) → C y → C (free_semigroup.of x * y)) → C x
Recursor for free semigroup using of and *.
Auxiliary function for free_semigroup.lift.
Equations
- free_semigroup.lift' f x (hd :: tl) = f x * free_semigroup.lift' f hd tl
- free_semigroup.lift' f x list.nil = f x
def
free_add_semigroup.lift'
{α : Type u}
{β : Type v}
[add_semigroup β] :
(α → β) → α → list α → β
Auxiliary function for free_semigroup.lift.
Equations
- free_add_semigroup.lift' f x (hd :: tl) = f x + free_add_semigroup.lift' f hd tl
- free_add_semigroup.lift' f x list.nil = f x
Lifts a function α → β to a semigroup homomorphism free_semigroup α → β given
a semigroup β.
Equations
- free_semigroup.lift f x = free_semigroup.lift' f x.fst x.snd
def
free_add_semigroup.lift
{α : Type u}
{β : Type v}
[add_semigroup β] :
(α → β) → free_add_semigroup α → β
Lifts a function α → β to an additive semigroup homomorphism
free_add_semigroup α → β given an additive semigroup β.
@[simp]
theorem
free_add_semigroup.lift_of
{α : Type u}
{β : Type v}
[add_semigroup β]
(f : α → β)
(x : α) :
free_add_semigroup.lift f (free_add_semigroup.of x) = f x
@[simp]
theorem
free_semigroup.lift_of
{α : Type u}
{β : Type v}
[semigroup β]
(f : α → β)
(x : α) :
free_semigroup.lift f (free_semigroup.of x) = f x
theorem
free_add_semigroup.lift_of_add
{α : Type u}
{β : Type v}
[add_semigroup β]
(f : α → β)
(x : α)
(y : free_add_semigroup α) :
free_add_semigroup.lift f (free_add_semigroup.of x + y) = f x + free_add_semigroup.lift f y
theorem
free_semigroup.lift_of_mul
{α : Type u}
{β : Type v}
[semigroup β]
(f : α → β)
(x : α)
(y : free_semigroup α) :
free_semigroup.lift f (free_semigroup.of x * y) = f x * free_semigroup.lift f y
@[simp]
theorem
free_semigroup.lift_mul
{α : Type u}
{β : Type v}
[semigroup β]
(f : α → β)
(x y : free_semigroup α) :
free_semigroup.lift f (x * y) = free_semigroup.lift f x * free_semigroup.lift f y
@[simp]
theorem
free_add_semigroup.lift_add
{α : Type u}
{β : Type v}
[add_semigroup β]
(f : α → β)
(x y : free_add_semigroup α) :
free_add_semigroup.lift f (x + y) = free_add_semigroup.lift f x + free_add_semigroup.lift f y
theorem
free_semigroup.lift_unique
{α : Type u}
{β : Type v}
[semigroup β]
(f : free_semigroup α → β) :
(∀ (x y : free_semigroup α), f (x * y) = f x * f y) → f = free_semigroup.lift (f ∘ free_semigroup.of)
theorem
free_add_semigroup.lift_unique
{α : Type u}
{β : Type v}
[add_semigroup β]
(f : free_add_semigroup α → β) :
(∀ (x y : free_add_semigroup α), f (x + y) = f x + f y) → f = free_add_semigroup.lift (f ∘ free_add_semigroup.of)
def
free_add_semigroup.map
{α : Type u}
{β : Type v} :
(α → β) → free_add_semigroup α → free_add_semigroup β
The unique additive semigroup homomorphism that sends of x to of (f x).
@[simp]
theorem
free_semigroup.map_of
{α : Type u}
{β : Type v}
(f : α → β)
(x : α) :
free_semigroup.map f (free_semigroup.of x) = free_semigroup.of (f x)
@[simp]
@[simp]
theorem
free_semigroup.map_mul
{α : Type u}
{β : Type v}
(f : α → β)
(x y : free_semigroup α) :
free_semigroup.map f (x * y) = free_semigroup.map f x * free_semigroup.map f y
@[simp]
theorem
free_add_semigroup.map_add
{α : Type u}
{β : Type v}
(f : α → β)
(x y : free_add_semigroup α) :
free_add_semigroup.map f (x + y) = free_add_semigroup.map f x + free_add_semigroup.map f y
@[instance]
Equations
def
free_semigroup.rec_on'
{α : Type u}
{C : free_semigroup α → Sort l}
(x : free_semigroup α) :
(Π (x : α), C (has_pure.pure x)) → (Π (x : α) (y : free_semigroup α), C (has_pure.pure x) → C y → C (has_pure.pure x * y)) → C x
Recursor that uses pure instead of of.
def
free_add_semigroup.rec_on'
{α : Type u}
{C : free_add_semigroup α → Sort l}
(x : free_add_semigroup α) :
(Π (x : α), C (has_pure.pure x)) → (Π (x : α) (y : free_add_semigroup α), C (has_pure.pure x) → C y → C (has_pure.pure x + y)) → C x
Recursor that uses pure instead of of.
@[simp]
theorem
free_add_semigroup.map_pure
{α β : Type u}
(f : α → β)
(x : α) :
f <$> has_pure.pure x = has_pure.pure (f x)
@[simp]
theorem
free_semigroup.map_pure
{α β : Type u}
(f : α → β)
(x : α) :
f <$> has_pure.pure x = has_pure.pure (f x)
@[simp]
@[simp]
@[simp]
theorem
free_semigroup.pure_bind
{α β : Type u}
(f : α → free_semigroup β)
(x : α) :
has_pure.pure x >>= f = f x
@[simp]
theorem
free_add_semigroup.pure_bind
{α β : Type u}
(f : α → free_add_semigroup β)
(x : α) :
has_pure.pure x >>= f = f x
@[simp]
theorem
free_add_semigroup.add_bind
{α β : Type u}
(f : α → free_add_semigroup β)
(x y : free_add_semigroup α) :
@[simp]
theorem
free_semigroup.mul_bind
{α β : Type u}
(f : α → free_semigroup β)
(x y : free_semigroup α) :
@[simp]
theorem
free_semigroup.pure_seq
{α β : Type u}
{f : α → β}
{x : free_semigroup α} :
has_pure.pure f <*> x = f <$> x
@[simp]
theorem
free_add_semigroup.pure_seq
{α β : Type u}
{f : α → β}
{x : free_add_semigroup α} :
has_pure.pure f <*> x = f <$> x
@[simp]
theorem
free_semigroup.mul_seq
{α β : Type u}
{f g : free_semigroup (α → β)}
{x : free_semigroup α} :
@[simp]
theorem
free_add_semigroup.add_seq
{α β : Type u}
{f g : free_add_semigroup (α → β)}
{x : free_add_semigroup α} :
@[instance]
Equations
def
free_add_semigroup.traverse
{m : Type u → Type u}
[applicative m]
{α β : Type u} :
(α → m β) → free_add_semigroup α → m (free_add_semigroup β)
free_add_semigroup is traversable.
def
free_semigroup.traverse
{m : Type u → Type u}
[applicative m]
{α β : Type u} :
(α → m β) → free_semigroup α → m (free_semigroup β)
free_semigroup is traversable.
Equations
- free_semigroup.traverse F x = x.rec_on' (λ (x : α), has_pure.pure <$> F x) (λ (x : α) (y : free_semigroup α) (ihx ihy : m (free_semigroup β)), has_mul.mul <$> ihx <*> ihy)
@[instance]
@[simp]
theorem
free_add_semigroup.traverse_pure
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
(x : α) :
traversable.traverse F (has_pure.pure x) = has_pure.pure <$> F x
@[simp]
theorem
free_semigroup.traverse_pure
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
(x : α) :
traversable.traverse F (has_pure.pure x) = has_pure.pure <$> F x
@[simp]
theorem
free_semigroup.traverse_pure'
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β) :
traversable.traverse F ∘ has_pure.pure = λ (x : α), has_pure.pure <$> F x
@[simp]
theorem
free_add_semigroup.traverse_pure'
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β) :
traversable.traverse F ∘ has_pure.pure = λ (x : α), has_pure.pure <$> F x
@[simp]
theorem
free_add_semigroup.traverse_add
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
[is_lawful_applicative m]
(x y : free_add_semigroup α) :
traversable.traverse F (x + y) = has_add.add <$> traversable.traverse F x <*> traversable.traverse F y
@[simp]
theorem
free_semigroup.traverse_mul
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
[is_lawful_applicative m]
(x y : free_semigroup α) :
traversable.traverse F (x * y) = has_mul.mul <$> traversable.traverse F x <*> traversable.traverse F y
@[simp]
theorem
free_add_semigroup.traverse_add'
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
[is_lawful_applicative m] :
function.comp (traversable.traverse F) ∘ has_add.add = λ (x y : free_add_semigroup α), has_add.add <$> traversable.traverse F x <*> traversable.traverse F y
@[simp]
theorem
free_semigroup.traverse_mul'
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
[is_lawful_applicative m] :
function.comp (traversable.traverse F) ∘ has_mul.mul = λ (x y : free_semigroup α), has_mul.mul <$> traversable.traverse F x <*> traversable.traverse F y
@[simp]
theorem
free_semigroup.traverse_eq
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
(x : free_semigroup α) :
@[simp]
theorem
free_add_semigroup.traverse_eq
{α β : Type u}
{m : Type u → Type u}
[applicative m]
(F : α → m β)
(x : free_add_semigroup α) :
@[simp]
theorem
free_semigroup.mul_map_seq
{α : Type u}
(x y : free_semigroup α) :
has_mul.mul <$> x <*> y = x * y
@[simp]
theorem
free_add_semigroup.add_map_seq
{α : Type u}
(x y : free_add_semigroup α) :
has_add.add <$> x <*> y = x + y
@[instance]
Equations
- free_semigroup.is_lawful_traversable = {to_is_lawful_functor := free_semigroup.is_lawful_traversable._proof_1, id_traverse := free_semigroup.is_lawful_traversable._proof_2, comp_traverse := free_semigroup.is_lawful_traversable._proof_3, traverse_eq_map_id := free_semigroup.is_lawful_traversable._proof_4, naturality := free_semigroup.is_lawful_traversable._proof_5}
@[instance]
@[instance]
Equations
Isomorphism between magma.free_semigroup (free_magma α) and free_semigroup α.
Equations
Isomorphism between
add_magma.free_add_semigroup (free_add_magma α) and free_add_semigroup α.
@[simp]
theorem
free_semigroup_free_magma_mul
{α : Type u}
(x y : magma.free_semigroup (free_magma α)) :
⇑(free_semigroup_free_magma α) (x * y) = ⇑(free_semigroup_free_magma α) x * ⇑(free_semigroup_free_magma α) y
@[simp]
theorem
free_add_semigroup_free_add_magma_add
{α : Type u}
(x y : add_magma.free_add_semigroup (free_add_magma α)) :
⇑(free_add_semigroup_free_add_magma α) (x + y) = ⇑(free_add_semigroup_free_add_magma α) x + ⇑(free_add_semigroup_free_add_magma α) y