Symbol frequency

Symbol frequencies for library suggestions are computed on first use, without storing any data in olean files. The first query may be expensive for large imported libraries. Index construction does not consume the caller's heartbeat budget, but can be interrupted.

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)