def Lean.Meta.mkGeneralizationForbiddenSet (targets : Array Lean.Expr) (forbidden : optParam Lean.FVarIdSet ∅) : Lean.MetaM Lean.FVarIdSet

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.

def Lean.Meta.mkGeneralizationForbiddenSet.visit (fvarId : Lean.FVarId) (todo : List Lean.FVarId) (s : Lean.FVarIdSet) : Lean.MetaM (List Lean.FVarId × Lean.FVarIdSet)

Equations

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

partial def Lean.Meta.mkGeneralizationForbiddenSet.loop (todo : List Lean.FVarId) (s : Lean.FVarIdSet) : Lean.MetaM Lean.FVarIdSet

def Lean.Meta.getFVarSetToGeneralize (targets : Array Lean.Expr) (forbidden : Lean.FVarIdSet) (ignoreLetDecls : optParam Bool false) : Lean.MetaM Lean.FVarIdSet

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 : Array Lean.Expr) (forbidden : optParam Lean.FVarIdSet ∅) (ignoreLetDecls : optParam Bool false) : Lean.MetaM (Array Lean.FVarId)

Equations

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