Lean4
/-- `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.
-/
@[command_parser 1000]
public meta def commandAssert_not_exists_ : Lean.ParserDescr✝ :=
ParserDescr.node✝ `commandAssert_not_exists_ 1022
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "assert_not_exists ")
(ParserDescr.unary✝ `many1 (ParserDescr.const✝ `ident)))
