Lean4
/-- If `α` is a type, then `FreeMagma α` is the free magma generated by `α`.
This is a magma equipped with a function `FreeMagma.of : α → FreeMagma α` which has
the following universal property: if `M` is any magma, and `f : α → M` is any function,
then this function is the composite of `FreeMagma.of` and a unique multiplicative homomorphism
`FreeMagma.lift f : FreeMagma α →ₙ* M`.
A typical element of `FreeMagma α` is a formal non-associative product of
elements of `α`. For example if `x` and `y` are terms of type `α` then `x * ((y * y) * x)` is a
"typical" element of `FreeMagma α`.
One can think of `FreeMagma α` as the type of binary trees with leaves labelled by `α`.
In general, no pair of distinct elements in `FreeMagma α` will commute.
-/
@[to_additive]
inductive FreeMagma (α : Type u) : Type u
| of : α → FreeMagma α
| mul : FreeMagma α → FreeMagma α → FreeMagma α
deriving DecidableEq
