def Lean.Meta.mkGeneralizationForbiddenSet (targets : Array Expr) (forbidden : FVarIdSet := ∅) : MetaM 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 : FVarId) (todo : List FVarId) (s : FVarIdSet) : MetaM (List FVarId × FVarIdSet)

Equations

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

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

def Lean.Meta.getFVarSetToGeneralize (targets : Array Expr) (forbidden : FVarIdSet) (ignoreLetDecls : Bool := false) : MetaM 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 Expr) (forbidden : FVarIdSet := ∅) (ignoreLetDecls : Bool := false) : MetaM (Array FVarId)

Equations

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