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 whether a declaration or an import is 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

Equations

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

def Mathlib.AssertNotExist.instBEqAssertExists.beq : AssertExists → AssertExists → Bool

Equations

• Mathlib.AssertNotExist.instBEqAssertExists.beq { isDecl := a, givenName := a_1, modName := a_2 } { isDecl := b, givenName := b_1, modName := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Mathlib.AssertNotExist.instBEqAssertExists.beq x✝¹ x✝ = false

def Mathlib.AssertNotExist.instHashableAssertExists.hash : AssertExists → UInt64

Equations

• Mathlib.AssertNotExist.instHashableAssertExists.hash { isDecl := a, givenName := a_1, modName := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

instance Mathlib.AssertNotExist.instHashableAssertExists : Hashable AssertExists

Equations

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

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

Defines the assertExistsExt extension for adding a HashSet of AssertExists entries 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 forbidden from existing/being 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 : 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.