Documentation

Lean.Meta.CollectMVars

Collect unassigned metavariables occuring in the given expression.

Remark: if e contains ?m and there is a t assigned to ?m, we collect unassigned metavariables occurring in t.

Remark: if e contains ?m and ?m is delayed assigned to some term t, we collect ?m and unassigned metavariables occurring in t. We collect ?m because it has not been assigned yet.

Return metavariables in occuring the given expression. See collectMVars

Equations
Instances For

    Similar to getMVars, but removes delayed assignments.

    Equations
    Instances For
      Equations
      Instances For