Documentation

Mathlib.Util.AssertExistsExt

Environment extension for tracking existence of declarations and imports #

This is used by the assert_not_exists and assert_not_imported commands.

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.

Instances For
    def Mathlib.AssertNotExist.addDeclEntry {m : TypeType} [Lean.MonadEnv m] (isDecl : Bool) (declName mod : Lean.Name) :

    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
      Instances For

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

        Equations
          Instances For