asFn

Mathlib.Tactic.Simps.Basic

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

Lean4

/-- A common configuration for `@[simps]`: generate equalities between functions instead equalities
between fully applied Expressions. Replaced by `@[simps -fullyApplied]`. -/
@[deprecated "use `-fullyApplied` instead" (since := "2025-03-10")]
def asFn : Simps.Config where fullyApplied := false

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

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

Разделы

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

Аффилиация

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