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 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 commandAssert_not_exists_ : Lean.ParserDescr

assert_not_exists n is a user command that asserts that a declaration named n does 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.

Equations

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