checking for unassigned mvars

Stream: Is there code for X?

[Siddhartha Gadgil]

I wrote the following code because I could not locate a function already in Lean, though I expect it is. Can someone point it out?

partial def Lean.Expr.hasUnassignedExprMVar (e: Expr) : MetaM Bool := do
  let deps ← getMVars e
  for m in deps do
    match (← getExprMVarAssignment? m) with
    | some e  =>
      if ←  e.hasUnassignedExprMVar then
        return true
    | none => return true
  return false

[Siddharth Bhat]

(deleted)

[Kyle Miller]

I'm pretty sure this is !(← getMVars e).isEmpty. The getMVars function is monadic because it instantiates mvars.

That collects all mvars accessible through delayed assignments though, which is more complicated than you need for this. (← instantiateMVars e).hasExprMVar does less work.