opaque Lean.noncomputableExt : TagDeclarationExtension

def Lean.addNoncomputable (env : Environment) (declName : Name) : Environment

Mark in the environment extension that the given declaration has been declared by the user as noncomputable.

Equations

• Lean.addNoncomputable env declName = Lean.noncomputableExt.tag env declName

def Lean.isNoncomputable (env : Environment) (declName : Name) (asyncMode : EnvExtension.AsyncMode := noncomputableExt.toEnvExtension.asyncMode) : Bool

Returns true when the given declaration is tagged noncomputable.

Equations

• Lean.isNoncomputable env declName asyncMode = Lean.noncomputableExt.isTagged env declName asyncMode