Documentation

Lean.Meta.GeneralizeVars

source
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.
source
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.
source
partial def Lean.Meta.mkGeneralizationForbiddenSet.loop (todo : List Lean.FVarId) (s : Lean.FVarIdSet) :
Lean.MetaM Lean.FVarIdSet
source
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.
source
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.