Def elabSuppressCompilationDecl

Modification history

2023-10-03 11:52
Mathlib/Tactic/SuppressCompilation.lean
feat: new tactic suppress_compilation, use it in OperatorNorm (#7326) …
Added elabSuppressCompilationDeclView on Github →