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

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.

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

Return metavariables occurring in the given expression. See `collectMVars`

Equations

- Lean.Meta.getMVars e = do let __discr ← (Lean.Meta.collectMVars e).run { } match __discr with | (fst, s) => pure s.result

Instances For

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

Similar to `getMVars`, but removes delayed assignments.

Equations

- Lean.Meta.getMVarsNoDelayed e = do let mvarIds ← Lean.Meta.getMVars e Array.filterM (fun (mvarId : Lean.MVarId) => not <$> mvarId.isDelayedAssigned) mvarIds

Instances For

source
def Lean.Meta.collectMVarsAtDecl (d : Declaration) :
StateRefT' IO.RealWorld CollectMVars.State MetaM Unit
Equations

- Lean.Meta.collectMVarsAtDecl d = d.forExprM Lean.Meta.collectMVars

Instances For

source
def Lean.Meta.getMVarsAtDecl (d : Declaration) :
MetaM (Array MVarId)
Equations

- Lean.Meta.getMVarsAtDecl d = do let __discr ← (Lean.Meta.collectMVarsAtDecl d).run { } match __discr with | (fst, s) => pure s.result

Instances For

source
def Lean.MVarId.getMVarDependencies (mvarId : MVarId) (includeDelayed : Bool := false) :
MetaM (Std.HashSet MVarId)

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

- mvarId.getMVarDependencies includeDelayed = (fun (x : Unit × Std.HashSet Lean.MVarId) => x.snd) <$> (go✝ mvarId includeDelayed).run ∅

Instances For

source
def Lean.Expr.getMVarDependencies (e : Expr) (includeDelayed : Bool := false) :
MetaM (Std.HashSet MVarId)

Collect the metavariables appearing in the expression `e`, including metavariables in the type or local context of any such metavariables, etc.

Equations

- e.getMVarDependencies includeDelayed = (fun (x : Unit × Std.HashSet Lean.MVarId) => x.snd) <$> (addMVars✝ e includeDelayed).run ∅

Instances For