recOnPure

Mathlib.Algebra.Free

URI: https://scilib.ai/kg/mathlib#FreeMagma.recOnPure

Lean4

/-- Recursor on `FreeMagma` using `pure` instead of `of`. -/
@[to_additive (attr := elab_as_elim) /-- Recursor on `FreeAddMagma` using `pure` instead of `of`. -/
    ]
protected def recOnPure {C : FreeMagma α → Sort l} (x) (ih1 : ∀ x, C (pure x)) (ih2 : ∀ x y, C x → C y → C (x * y)) :
    C x :=
  FreeMagma.recOnMul x ih1 ih2

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru