Documentation

Lean.Compiler.NoncomputableAttr

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

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

      Return true iff the user has declared the given declaration as noncomputable.

      Equations
        Instances For