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 Mathlib.AssertNotExist.AssertExists

Equations

• Mathlib.AssertNotExist.instBEqAssertExists = { beq := Mathlib.AssertNotExist.beqAssertExists✝ }

instance Mathlib.AssertNotExist.instHashableAssertExists : Hashable Mathlib.AssertNotExist.AssertExists

Equations

• Mathlib.AssertNotExist.instHashableAssertExists = { hash := Mathlib.AssertNotExist.hashAssertExists✝ }

opaque Mathlib.AssertNotExist.assertExistsExt : Lean.SimplePersistentEnvExtension Mathlib.AssertNotExist.AssertExists (Std.HashSet Mathlib.AssertNotExist.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.

Equations

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

def Lean.Environment.getSortedAssertExists (env : Lean.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.

Equations

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