# Documentation

Lean.Meta.GeneralizeVars

def Lean.Meta.mkGeneralizationForbiddenSet (targets : ) (forbidden : ) :

Add to forbidden all a set of FVarIds containing targets and all variables they depend on.

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.getFVarSetToGeneralize (targets : ) (forbidden : Lean.FVarIdSet) (ignoreLetDecls : ) :

Collect variables to be generalized. It uses the following heuristic

• Collect forward dependencies that are not in the forbidden set, and depend on some variable in targets.

• We use mkForbiddenSet to compute forbidden.

Remark: we not collect instance implicit arguments nor auxiliary declarations for compiling recursive declarations.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Meta.getFVarsToGeneralize (targets : ) (forbidden : ) (ignoreLetDecls : ) :
Equations
• One or more equations did not get rendered due to their size.