Documentation

Lean.Compiler.NoncomputableAttr

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

Equations
@[export lean_is_noncomputable]
def Lean.isNoncomputable (env : Environment) (declName : Name) :

Returns true when the given declaration is tagged noncomputable.

Equations