change elaboration strategy with `by apply`

Mathlib.Algebra.Category.Ring.Limits

URI: https://scilib.ai/kg/mathlib#Mathlib.LibraryNote.change elaboration strategy with `by apply`

Lean4

/-- Some definitions may be extremely slow to elaborate, when the target type to be constructed
is complicated and when the type of the term given in the definition is also complicated and does
not obviously match the target type. In this case, instead of just giving the term, prefixing it
with `by apply` may speed up things considerably as the types are not elaborated in the same order.
-/
def «change elaboration strategy with `by apply`» : LibraryNote✝ :=
  ()

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

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

Разделы

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

Аффилиация

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