lemmasOnly

Mathlib.Tactic.Simps.Basic

URI: https://scilib.ai/kg/mathlib#Simps.Config.lemmasOnly

Lean4

/-- A common configuration for `@[simps]`: don't tag the generated lemmas with `@[simp]`.
Replaced by `@[simps -isSimp]`. -/
@[deprecated "use `-isSimp` instead" (since := "2025-03-10")]
def lemmasOnly : Config where isSimp := false

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

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

Разделы

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

Аффилиация

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