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.

Equations

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

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).

Equations

• Lean.LibrarySuggestions.localSymbolFrequency n = do let __do_lift ← Lean.LibrarySuggestions.cachedLocalSymbolFrequencyMap✝ pure (Std.TreeMap.getD __do_lift n 0)

def Lean.Environment.unsafeRunMetaM {α : Type} [Inhabited α] (env : Environment) (x : MetaM α) : α

Helper function for running MetaM code during module export, when there is nothing but an Environment available. Panics on errors.

Equations

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

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

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

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)