Environment extension for tracking existence of declarations and imports

This is used by the assert_not_exists and assert_not_imported commands.

structure Mathlib.AssertNotExist.AssertExists : Type

AssertExists is the structure that carries the data to check if a declaration or an import are meant to exist somewhere in Mathlib.

• isDecl : Bool

  The type of the assertion: true means declaration, false means import.

• givenName : Lean.Name

  The fully qualified name of a declaration that is expected to exist.

• modName : Lean.Name

  The name of the module where the assertion was made.

instance Mathlib.AssertNotExist.instBEqAssertExists : BEq AssertExists

instance Mathlib.AssertNotExist.instHashableAssertExists : Hashable AssertExists

opaque Mathlib.AssertNotExist.assertExistsExt : Lean.SimplePersistentEnvExtension AssertExists (Std.HashSet AssertExists)

Defines the assertExistsExt extension for adding a HashSet of AssertExistss to the environment.

def Mathlib.AssertNotExist.addDeclEntry {m : Type → Type} [Lean.MonadEnv m] (isDecl : Bool) (declName mod : Lean.Name) : m Unit

addDeclEntry isDecl declName mod takes as input the Boolean isDecl and the Names of a declaration or import, declName, and of a module, mod. It extends the AssertExists environment extension with the data isDecl, declName, mod. This information is used to capture declarations and modules that are required to not exist/be imported at some point, but should eventually exist/be imported.

def Lean.Environment.getSortedAssertExists (env : Environment) : Array Mathlib.AssertNotExist.AssertExists

getSortedAssertExists env returns the array of AssertExists, placing first all declarations, in alphabetical order, and then all modules, also in alphabetical order.