countHeartbeats

Mathlib.Util.CountHeartbeats

URI: https://scilib.ai/kg/mathlib#Mathlib.Linter.linter.countHeartbeats

Lean4

/-- The "countHeartbeats" linter counts the heartbeats of every declaration.

The effect of the linter is similar to `#count_heartbeats in xxx`, except that it applies
to all declarations.

Note that the linter only counts heartbeats in "top-level" declarations:
it looks inside `set_option ... in`, but not, for instance, inside `mutual` blocks.

There is a convenience notation `#count_heartbeats` that simply sets the linter option to true.
-/
@[init initFn✝, ]
opaque countHeartbeats : Lean.Option✝ Bool

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

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

Разделы

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

Аффилиация

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