instance Lean.NameSet.instSingletonName_importGraph : Singleton Lean.Name Lean.NameSet

Equations

• Lean.NameSet.instSingletonName_importGraph = { singleton := fun (n : Lean.Name) => ∅.insert n }

instance Lean.NameSet.instUnion_importGraph : Union Lean.NameSet

Equations

• Lean.NameSet.instUnion_importGraph = { union := fun (s t : Lean.NameSet) => Lean.RBTree.fold (fun (t : Lean.NameSet) (n : Lean.Name) => t.insert n) t s }

instance Lean.NameSet.instInter_importGraph : Inter Lean.NameSet

Equations

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

instance Lean.NameSet.instSDiff_importGraph : SDiff Lean.NameSet

Equations

• Lean.NameSet.instSDiff_importGraph = { sdiff := fun (s t : Lean.NameSet) => Lean.RBTree.fold (fun (s : Lean.NameSet) (n : Lean.Name) => Lean.RBTree.erase s n) s t }

def Lean.NameSet.ofList (l : List Lean.Name) : Lean.NameSet

Equations

• Lean.NameSet.ofList l = List.foldl (fun (s : Lean.NameSet) (n : Lean.Name) => s.insert n) ∅ l

def Lean.NameSet.ofArray (a : Array Lean.Name) : Lean.NameSet

Equations

• Lean.NameSet.ofArray a = Array.foldl (fun (s : Lean.NameSet) (n : Lean.Name) => s.insert n) ∅ a

def Lean.Environment.getModuleFor? (env : Lean.Environment) (declName : Lean.Name) : Option Lean.Name

Return the name of the module in which a declaration was defined.

Equations

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

def Lean.Name.requiredModules (n : Lean.Name) : Lean.CoreM Lean.NameSet

Return the names of the modules in which constants used in the specified declaration were defined.

Note that this will not account for tactics and syntax used in the declaration, so the results may not suffice as imports.

Equations

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

def Lean.NameSet.transitivelyUsedConstants (s : Lean.NameSet) : Lean.CoreM Lean.NameSet

Return the names of the constants used in the specified declarations, and the constants they use transitively.

Equations

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

def Lean.Name.transitivelyUsedConstants (n : Lean.Name) : Lean.CoreM Lean.NameSet

Return the names of the constants used in the specified declaration, and the constants they use transitively.

Equations

• n.transitivelyUsedConstants = {n}.transitivelyUsedConstants

def Lean.NameSet.transitivelyRequiredModules (s : Lean.NameSet) (env : Lean.Environment) : Lean.CoreM Lean.NameSet

Return the names of the modules in which constants used transitively in the specified declarations were defined.

Note that this will not account for tactics and syntax used in the declaration, so the results may not suffice as imports.

Equations

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

def Lean.Name.transitivelyRequiredModules (n : Lean.Name) (env : Lean.Environment) : Lean.CoreM Lean.NameSet

Return the names of the modules in which constants used transitively in the specified declaration were defined.

Note that this will not account for tactics and syntax used in the declaration, so the results may not suffice as imports.

Equations

• n.transitivelyRequiredModules env = {n}.transitivelyRequiredModules env

def Lean.Environment.transitivelyRequiredModules (env : Lean.Environment) (module : Lean.Name) : Lean.CoreM Lean.NameSet

Finds all constants defined in the specified module, and identifies all modules containing constants which are transitively required by those constants.

Equations

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

def Lean.Environment.transitivelyRequiredModules' (env : Lean.Environment) (modules : List Lean.Name) (verbose : optParam Bool false) : Lean.CoreM (Lean.NameMap Lean.NameSet)

Computes all the modules transitively required by the specified modules. Should be equivalent to calling transitivelyRequiredModules on each module, but shares more of the work.

Equations

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

def Lean.Environment.transitivelyRequiredModules'.toBitVec (env : Lean.Environment) {N : Nat} (s : Lean.NameSet) : BitVec N

Equations

• Lean.Environment.transitivelyRequiredModules'.toBitVec env s = Lean.RBTree.fold (fun (b : BitVec N) (n : Lean.Name) => b ||| BitVec.twoPow N ((env.header.moduleNames.getIdx? n).getD 0)) 0 s

def Lean.Environment.transitivelyRequiredModules'.toNameSet (env : Lean.Environment) {N : Nat} (b : BitVec N) : Lean.NameSet

Equations

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

def Lean.Environment.requiredModules (env : Lean.Environment) : Lean.NameSet

Return the names of the modules in which constants used in the current file were defined.

Note that this will not account for tactics and syntax used in the file, so the results may not suffice as imports.

Equations

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