opaque Lean.noncomputableExt : Lean.TagDeclarationExtension

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

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

def Lean.isNoncomputable (env : Lean.Environment) (declName : Lake.Name) : Bool

Return true iff the user has declared the given declaration as noncomputable. Remark: we use this function only for introspection. It is currently not used by the code generator.