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. -/
def elabSuppressCompilationDecl : CommandElab := fun
|
`($[$doc?:docComment]?$(attrs?)
?$(vis?)?$[noncomputable ]?$(unsafe?)?$(recKind?)?def $id$sig:optDeclSig$val:declVal) =>
do
elabDeclaration <|
←
`($[$doc?:docComment]?$(attrs?)
?$(vis?)?noncomputable $(unsafe?)?$(recKind?)?def $id$sig:optDeclSig$val:declVal)
|
`($[$doc?:docComment]?$(attrs?)
?$(vis?)?$[noncomputable ]?$(unsafe?)?$(recKind?)?def $id$sig:optDeclSig$val:declVal
deriving $derivs,*) =>
do
elabDeclaration <|
←
`($[$doc?:docComment]?$(attrs?)
?$(vis?)?noncomputable $(unsafe?)?$(recKind?)?def $id$sig:optDeclSig$val:declVal
deriving $derivs,*)
|
`($[$doc?:docComment]?$(attrs?)
?$(vis?)?$[noncomputable ]?$(unsafe?)?$(recKind?)?$(attrKind?)?instance$(prio?)?
$(id?)?$sig:declSig$val:declVal) =>
do
elabDeclaration <|
←
`($[$doc?:docComment]?$(attrs?)
?$(vis?)?noncomputable $(unsafe?)?$(recKind?)?$(attrKind?)?instance$(prio?)?
$(id?)?$sig:declSig$val:declVal)
|
`($[$doc?:docComment]?$(attrs?)
?$(vis?)?$[noncomputable ]?$(unsafe?)?$(recKind?)?example$sig:optDeclSig$val:declVal) =>
do
elabDeclaration <|
←
`($[$doc?:docComment]?$(attrs?)
?$(vis?)?noncomputable $(unsafe?)?$(recKind?)?example$sig:optDeclSig$val:declVal)
|
`($[$doc?:docComment]?$(attrs?)
?$(vis?)?$[noncomputable ]?$(unsafe?)?$(recKind?)?abbrev $id$sig:optDeclSig$val:declVal) =>
do
elabDeclaration <|
←
`($[$doc?:docComment]?$(attrs?)
?$(vis?)?noncomputable $(unsafe?)?$(recKind?)?abbrev $id$sig:optDeclSig$val:declVal)
| _ => throwUnsupportedSyntax
