Symbol frequency

This module provides a persistent environment extension for computing the frequency of symbols in the environment.

def Lean.LibrarySuggestions.localSymbolFrequencyMap : MetaM (NameMap Nat)

Collect the frequencies for constants occurring in declarations defined in the current module, skipping instance arguments and proofs.

def Lean.LibrarySuggestions.localSymbolFrequency (n : Name) : MetaM Nat

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

Note that this is cached, and so returns the frequency within theorems that had been elaborated when the function is first called (with any argument).

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

The symbol frequency map for imported constants. This is initialized on first use.

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.