# User commands to assert the (non-)existence of declarations or instances. #

These commands are used to enforce the independence of different parts of mathlib.

## TODO #

Potentially reimplement the mathlib 3 linters to check that declarations asserted not to exist do eventually exist.

Implement `assert_instance` and `assert_no_instance`.

source
def Mathlib.AssertNotExist.«command#check_assertions!» :
Lean.ParserDescr

`#check_assertions` retrieves all declarations and all imports that were declared not to exist so far (including in transitively imported files) and reports their current status:

- ✓ means the declaration or import exists,
- × means the declaration or import does not exist.

This means that the expectation is that all checks succeed by the time `#check_assertions` is used, typically once all of `Mathlib` has been built.

If all declarations and imports are available when `#check_assertions` is used, then the command logs an info message. Otherwise, it emits a warning.

The variant `#check_assertions!` only prints declarations/imports that are not present in the environment. In particular, it is silent if everything is imported, making it useful for testing.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def commandAssert_exists_ :
Lean.ParserDescr

`assert_exists n` is a user command that asserts that a declaration named `n` exists in the current import scope.

Be careful to use names (e.g. `Rat`) rather than notations (e.g. `ℚ`).

Equations

- commandAssert_exists_ = Lean.ParserDescr.node `commandAssert_exists_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "assert_exists ") (Lean.ParserDescr.const `ident))

Instances For

source
def importPathMessage (env : Lean.Environment) (idx : Lean.ModuleIdx) :
Lean.MessageData

`importPathMessage env idx` produces a message laying out an import chain from `idx` to the current module. The output is of the form

    Mathlib.Init,
      which is imported by Mathlib.Util.AssertExistsExt,
      which is imported by Mathlib.Util.AssertExists,
      which is imported by this file.

if `env` is an `Environment` and `idx` is the module index of `Mathlib.Init`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def commandAssert_not_exists_ :
Lean.ParserDescr

`assert_not_exists d₁ d₂ ... dₙ` is a user command that asserts that the declarations named `d₁ d₂ ... dₙ` do not exist in the current import scope.

Be careful to use names (e.g. `Rat`) rather than notations (e.g. `ℚ`).

It may be used (sparingly!) in mathlib to enforce plans that certain files are independent of each other.

If you encounter an error on an `assert_not_exists` command while developing mathlib, it is probably because you have introduced new import dependencies to a file.

In this case, you should refactor your work (for example by creating new files rather than adding imports to existing files). You should not delete the `assert_not_exists` statement without careful discussion ahead of time.

`assert_not_exists` statements should generally live at the top of the file, after the module doc.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def commandAssert_not_imported_ :
Lean.ParserDescr

`assert_not_imported m₁ m₂ ... mₙ` checks that each one of the modules `m₁ m₂ ... mₙ` is not among the transitive imports of the current file.

The command does not currently check whether the modules `m₁ m₂ ... mₙ` actually exist.

Equations

- One or more equations did not get rendered due to their size.

Instances For