pendingActionableSynthMVar — Mathlib

Lean4

/-- Find a synthetic typeclass metavariable with no expr metavariables in its type. -/
def pendingActionableSynthMVar (binder : TSyntax ``bracketedBinder) : TermElabM (Option MVarId) := do
  let pendingMVars := (← get).pendingMVars
  if pendingMVars.isEmpty then
    return none
  for mvarId in pendingMVars.reverse do
    let some decl ← Term.getSyntheticMVarDecl? mvarId |
      continue
    match decl.kind with
    | .typeClass _ =>
      let ty ← instantiateMVars (← mvarId.getType)
      if !ty.hasExprMVar then
        return mvarId
    | _ =>
      pure ()
  throwErrorAt binder "Cannot satisfy requirements for {binder} due to metavariables."

Похожие утверждения