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