Symbol frequency

Symbol frequencies for library suggestions are computed on first use and cached for the process. The imported statements are traversed in parallel tasks. Index construction does not count against the caller's heartbeat budget. Cancellation is checked during traversal and while waiting for another caller's computation. Once their inputs are available, the frequency and trigger maps are built without further cancellation checks, so later queries can reuse the cached results.

def Lean.LibrarySuggestions.symbolFrequencyMap : CoreM (NameMap Nat)

The symbol frequency map for imported constants. This is computed and cached on first use, assuming the imported environment remains fixed for the lifetime of the process. Local declarations are not included.

Equations

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

def Lean.LibrarySuggestions.symbolFrequency (n : Name) : CoreM Nat

Return the number of times a Name appears in the signatures of (non-internal) theorems in the imported environment, skipping instance arguments and proofs.

Equations

• Lean.LibrarySuggestions.symbolFrequency n = do let __do_lift ← Lean.LibrarySuggestions.symbolFrequencyMap pure (Std.TreeMap.getD __do_lift n 0)