recOnPure

Mathlib.Algebra.Free

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

Lean4

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

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

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

Разделы

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

Аффилиация

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