commandAssert_not_imported_ — Mathlib

Lean4

/-- `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.
-/
-- TODO: make sure that each one of `m₁ m₂ ... mₙ` is the name of an actually existing module!

@[command_parser 1000]
public meta def commandAssert_not_imported_ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `commandAssert_not_imported_ 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "assert_not_imported ")
      (ParserDescr.unary✝ `many1 (ParserDescr.const✝ `ident)))

Похожие утверждения