Infrastructure for recording extra import dependencies not implied by the environment constants for the benefit of shake.

structure Lean.ExtraModUse : Type

Additional import dependency for elaboration.

• module : Name

  Dependency's module name.

• isExported : Bool

  Whether dependency must be imported as public.

• isMeta : Bool

  Whether dependency must be imported as meta.

def Lean.instBEqExtraModUse.beq : ExtraModUse → ExtraModUse → Bool

Equations

• Lean.instBEqExtraModUse.beq { module := a, isExported := a_1, isMeta := a_2 } { module := b, isExported := b_1, isMeta := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.instBEqExtraModUse.beq x✝¹ x✝ = false

instance Lean.instBEqExtraModUse : BEq ExtraModUse

Equations

• Lean.instBEqExtraModUse = { beq := Lean.instBEqExtraModUse.beq }

def Lean.instHashableExtraModUse.hash : ExtraModUse → UInt64

Equations

• Lean.instHashableExtraModUse.hash { module := a, isExported := a_1, isMeta := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

instance Lean.instHashableExtraModUse : Hashable ExtraModUse

Equations

• Lean.instHashableExtraModUse = { hash := Lean.instHashableExtraModUse.hash }

instance Lean.instReprExtraModUse : Repr ExtraModUse

Equations

• Lean.instReprExtraModUse = { reprPrec := Lean.instReprExtraModUse.repr }

def Lean.instReprExtraModUse.repr : ExtraModUse → Nat → Format

Equations

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

def Lean.getExtraModUses (env : Environment) (modIdx : ModuleIdx) : Array ExtraModUse

Returns additional recorded import dependencies of the given module.

Equations

• Lean.getExtraModUses env modIdx = Lean.PersistentEnvExtension.getModuleEntries Lean.extraModUses✝ env modIdx

def Lean.copyExtraModUses (src dest : Environment) : Environment

Copies additional recorded import dependencies from one environment to another.

Equations

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

def Lean.recordExtraModUse {m : Type → Type} [Monad m] [MonadEnv m] [MonadTrace m] [MonadOptions m] [MonadRef m] [AddMessageContext m] (modName : Name) (isMeta : Bool) : m Unit

Records an additional import dependency for the current module, using Environment.isExporting as the visibility level.

Equations

• Lean.recordExtraModUse modName isMeta = do let __do_lift ← Lean.getEnv if (modName != __do_lift.mainModule) = true then Lean.recordExtraModUseCore✝ modName isMeta else pure PUnit.unit

def Lean.recordExtraModUseFromDecl {m : Type → Type} [Monad m] [MonadEnv m] [MonadTrace m] [MonadOptions m] [MonadRef m] [AddMessageContext m] (declName : Name) (isMeta : Bool) : m Unit

Records the module of the given declaration as an additional import dependency for the current module, using Environment.isExporting as the visibility level. If the declaration itself is already meta, the module dependency is recorded as a non-meta dependency.

Equations

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

def Lean.isExtraRevModUse (env : Environment) (modIdx : ModuleIdx) : Bool

Checks whether this module should be preserved as an import by shake.

Equations

• Lean.isExtraRevModUse env modIdx = !(Lean.PersistentEnvExtension.getModuleEntries Lean.isExtraRevModUseExt✝ env modIdx).isEmpty

def Lean.recordExtraRevUseOfCurrentModule {m : Type → Type} [Monad m] [MonadEnv m] : m Unit

Records this module to be preserved as an import by shake.

Equations

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