# Documentation

Lean.Elab.SyntheticMVars

def Lean.Elab.Term.reportStuckSyntheticMVar (mvarId : Lean.MVarId) (ignoreStuckTC : ) :

We use this method to report typeclass (and coercion) resolution problems that are "stuck". That is, there is nothing else to do, and we don't have enough information to synthesize them using TC resolution.

Equations
• One or more equations did not get rendered due to their size.
partial def Lean.Elab.Term.runTactic (mvarId : Lean.MVarId) (tacticCode : Lean.Syntax) :

Try to synthesize a term val using the tactic code tacticCode, and then assign mvarId := val.

partial def Lean.Elab.Term.synthesizeSyntheticMVars (mayPostpone : ) (ignoreStuckTC : ) :

Try to process pending synthetic metavariables. If mayPostpone == false, then pendingMVars is [] after executing this method.

It keeps executing synthesizeSyntheticMVarsStep while progress is being made. If mayPostpone == false, then it applies default instances to SyntheticMVarKind.typeClass (if available) metavariables that are still unresolved, and then tries to resolve metavariables with mayPostpone == false. That is, we force them to produce error messages and/or commit to a "best option". If, after that, we still haven't made progress, we report "stuck" errors.

Remark: we set ignoreStuckTC := true when elaborating simp arguments. Then, pending TC problems become implicit parameters for the simp theorem.

partial def Lean.Elab.Term.synthesizeSyntheticMVars.loop (mayPostpone : ) (ignoreStuckTC : ) :
@[inline]
def Lean.Elab.Term.withSynthesize {m : TypeType u_1} {α : Type} [inst : ] [inst : ] (k : m α) (mayPostpone : ) :
m α

Execute k, and synthesize pending synthetic metavariables created while executing k are solved. If mayPostpone == false, then all of them must be synthesized. Remark: even if mayPostpone == true, the method still uses synthesizeUsingDefault

Equations
@[inline]
def Lean.Elab.Term.withSynthesizeLight {m : TypeType u_1} {α : Type} [inst : ] [inst : ] (k : m α) :
m α

Similar to withSynthesize, but sets mayPostpone to true, and do not use synthesizeUsingDefault

Equations
def Lean.Elab.Term.elabTermAndSynthesize (stx : Lean.Syntax) (expectedType? : ) :

Elaborate stx, and make sure all pending synthetic metavariables created while elaborating stx are solved.

Equations
• One or more equations did not get rendered due to their size.

Collect unassigned metavariables at e that have associated tactic blocks, and then execute them using runTactic. We use this method at the match .. with elaborator when it cannot be postponed anymore, but it is still waiting the result of a tactic block.

Equations
• One or more equations did not get rendered due to their size.