Documentation

Lean.AddDecl

Adds given declaration to the environment, respecting debug.skipKernelTC.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Returns the kind of the declaration as originally declared instead of as exported. This information is stored by Lean.addDecl and may be inaccurate if that function was circumvented. Returns none if the declaration was not found.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Checks whether the declaration was originally declared as a theorem; see also Lean.getOriginalConstKind?. Returns false if the declaration was not found.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        If warn.sorry is set to true, then, so long as the message log does not already have any errors, declarations with sorryAx generate the "declaration uses 'sorry'" warning.

        If the warn.sorry option is set to true and there are no errors in the log already, logs a warning if the declaration uses sorry.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Lean.addDecl (decl : Declaration) (forceExpose : Bool := false) :

          Adds the given declaration to the environment's private scope, deriving a suitable presentation in the public scope if under the module system and if the declaration is not private. If forceExpose is true, exposes the declaration body, i.e. preserves the full representation in the public scope, independently of Environment.isExporting and even for theorems.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Lean.addAndCompile (decl : Declaration) (logCompileErrors : Bool := true) :
            Equations
            Instances For