higherOrderAttr

Mathlib.Tactic.HigherOrder

URI: https://scilib.ai/kg/mathlib#Tactic.higherOrderAttr

Lean4

/-- The `higher_order` attribute. From a lemma of the shape `∀ x, f (g x) = h x` derive an
auxiliary lemma of the form `f ∘ g = h` for reasoning about higher-order functions.

Syntax: `[higher_order]` or `[higher_order name]` where the given name is used for the
generated theorem. -/
@[init initFn✝, ]
opaque higherOrderAttr : ParametricAttribute Name

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

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

Разделы

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

Аффилиация

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