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