Lean4
/-- The command `unsuppress_compilation in def foo : ...` makes sure that the definition is
compiled to executable code, even if `suppress_compilation` is active. -/
@[macro commandUnsuppress_compilationIn_]
public meta def _aux_Mathlib_Tactic_SuppressCompilation___macroRules_commandUnsuppress_compilationIn__1 : Macro✝ := fun
| `(unsuppress_compilation$[ in $cmd?]?) => do
let declElab := mkCIdent ``elabSuppressCompilationDecl
let notaMacro := mkCIdent ``expandSuppressCompilationNotation
let attrCmds ← `(attribute [-command_elab] $declElab attribute [-macro] $notaMacro)
if let some cmd := cmd? then
`($attrCmds:command$cmd:command suppress_compilation)
else
return attrCmds
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
