English
Recursor for FreeMonoid: to prove a property C on any free word xs, it suffices to prove it for the unit and show that C is preserved by left multiplication by of x.
Русский
Рекурсор для FreeMonoid: чтобы доказать свойство C на любом слове, достаточно доказать на единице и показать, что C сохраняется при левой свертке на of x.
LaTeX
$$$\\\\forall C : FreeMonoid α \\\\to \\\\mathrm{Sort}*, \\\\; C(1) \\\\to \\\\; (\\\\forall x \\\\in \alpha, \\\\; C\\\\,(of x * xs)) \\\\to \\\\; C(xs)$$$
Lean4
/-- Recursor for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of `[]` and `x :: xs`. -/
@[to_additive (attr := elab_as_elim, induction_eliminator) /-- Recursor for `FreeAddMonoid` using `0` and
FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`. -/
]
-- Porting note: change from `List.recOn` to `List.rec` since only the latter is computable
def recOn {C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1) (ih : ∀ x xs, C xs → C (of x * xs)) : C xs :=
List.rec h0 ih xs
