commandSuppress_compilation

Mathlib.Tactic.SuppressCompilation

URI: https://scilib.ai/kg/mathlib#commandSuppress_compilation

Lean4

/-- Replacing `def` and `instance` by `noncomputable def` and `noncomputable instance`, designed
to disable the compiler in a given file or a given section.
This is a hack to work around https://github.com/leanprover-community/mathlib4/issues/7103.
Note that it does not work with `notation3`. You need to prefix such a notation declaration with
`unsuppress_compilation` if `suppress_compilation` is active. -/
@[command_parser 1000]
public meta def commandSuppress_compilation : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `commandSuppress_compilation 1024 (ParserDescr.symbol✝ "suppress_compilation")

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

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

Разделы

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

Аффилиация

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