Documentation

Lean.Meta.GeneralizeVars

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

Equations
    Instances For
      def Lean.Meta.getFVarSetToGeneralize (targets : Array Expr) (forbidden : FVarIdSet) (ignoreLetDecls : Bool := false) :

      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
        Instances For
          def Lean.Meta.getFVarsToGeneralize (targets : Array Expr) (forbidden : FVarIdSet := ) (ignoreLetDecls : Bool := false) :
          Equations
            Instances For