mathlib3 documentation

tactic.assert_exists

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

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

Implementation notes #

This file provides two linters that verify that things we assert do not yet exist do eventually exist. This works by creating declarations of the form:

These declarations are then picked up by the linter and analyzed accordingly. The _ in the _checked prefix should hide them from doc-gen.

source
meta def assert_exists (_x : interactive.parse (lean.parser.tk "assert_exists")) :
lean.parser unit

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

source
meta def assert_not_exists (_x : interactive.parse (lean.parser.tk "assert_not_exists")) :
lean.parser unit

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.

source
meta def assert_not_exists.linter  :
linter

A linter for checking that the declarations marked assert_not_exists eventually exist.

source
meta def assert_instance (_x : interactive.parse (lean.parser.tk "assert_instance")) :
lean.parser unit

assert_instance e is a user command that asserts that an instance e is available in the current import scope.

Example usage:

assert_instance semiring ℕ
source
meta def assert_no_instance (_x : interactive.parse (lean.parser.tk "assert_no_instance")) :
lean.parser unit

assert_no_instance e is a user command that asserts that an instance e is not available in the current import scope.

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_no_instance 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_no_instance statement without careful discussion ahead of time.

Example usage:

assert_no_instance linear_ordered_field ℚ
source
meta def assert_no_instance.linter  :
linter

A linter for checking that the declarations marked assert_no_instance eventually exist.