# Environment extension for tracking existence of declarations and imports #

This is used by the `assert_not_exists` and `assert_not_imported` commands.

source
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.

Instances For

source
instance Mathlib.AssertNotExist.instBEqAssertExists :
BEq AssertExists
Equations

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

source
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

Instances For

source
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)

Instances For

source
instance Mathlib.AssertNotExist.instHashableAssertExists :
Hashable AssertExists
Equations

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

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

Defines the `assertExistsExt` extension for adding a `HashSet` of `AssertExists` entries to the environment.

source
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 `Bool`ean `isDecl` and the `Name`s 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.

Instances For

source
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.

Instances For