User commands for assert the (non-)existence of declaration or instances.

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

TODO

Potentially after the port reimplement the mathlib 3 linters to check that declarations asserted about do eventually exist.

Implement assert_instance and assert_no_instance

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. 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.

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))

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.

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.

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.