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
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
Equations
- Lean.addAndCompile decl logCompileErrors = do Lean.addDecl decl Lean.compileDecl decl logCompileErrors