Documentation

Lean.Meta.GeneralizeVars

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

Instances For

    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.

    Instances For