Documentation

Lean.Meta.CollectMVars

Collect unassigned metavariables occurring 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 occurring in the given expression. See collectMVars

Equations
    Instances For

      Similar to getMVars, but removes delayed assignments.

      Equations
        Instances For
          Equations
            Instances For
              def Lean.MVarId.getMVarDependencies (mvarId : MVarId) (includeDelayed : Bool := false) :

              Collect the metavariables which mvarId depends on. These are the metavariables which appear in the type and local context of mvarId, as well as the metavariables which those metavariables depend on, etc.

              Equations
                Instances For

                  Auxiliary definition for getMVarDependencies.