Documentation

Lean.Compiler.NoncomputableAttr

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

Equations
Instances For

    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.

    Equations
    Instances For