Documentation

Lean.Compiler.NoncomputableAttr

source
opaque Lean.noncomputableExt :
TagDeclarationExtension
source
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.

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

    Returns true when the given declaration is tagged noncomputable.

    Instances For