Documentation

Lean.Meta.CollectMVars

source
partial def Lean.Meta.collectMVars (e : Lean.Expr) :
StateRefT' IO.RealWorld Lean.CollectMVars.State Lean.MetaM Unit

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.

source
def Lean.Meta.getMVars (e : Lean.Expr) :
Lean.MetaM (Array Lean.MVarId)

Return metavariables in occuring the given expression. See collectMVars

Instances For
    source
    def Lean.Meta.getMVarsNoDelayed (e : Lean.Expr) :
    Lean.MetaM (Array Lean.MVarId)

    Similar to getMVars, but removes delayed assignments.

    Instances For
      source
      def Lean.Meta.collectMVarsAtDecl (d : Lean.Declaration) :
      StateRefT' IO.RealWorld Lean.CollectMVars.State Lean.MetaM Unit
      Instances For
        source
        def Lean.Meta.getMVarsAtDecl (d : Lean.Declaration) :
        Lean.MetaM (Array Lean.MVarId)
        Instances For