def Lean.Elab.Term.reportStuckSyntheticMVar (mvarId : Lean.MVarId) (ignoreStuckTC : optParam Bool false) : Lean.Elab.TermElabM Unit

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) : Lean.Elab.TermElabM Unit

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

partial def Lean.Elab.Term.synthesizeSyntheticMVars (mayPostpone : optParam Bool true) (ignoreStuckTC : optParam Bool false) : Lean.Elab.TermElabM Unit

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 : optParam Bool true) (ignoreStuckTC : optParam Bool false) : Unit → Lean.Elab.TermElabM Unit

def Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC : optParam Bool false) : Lean.Elab.TermElabM Unit

Equations

• Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing ignoreStuckTC = Lean.Elab.Term.synthesizeSyntheticMVars false ignoreStuckTC

def Lean.Elab.Term.synthesizeSyntheticMVarsUsingDefault : Lean.Elab.TermElabM Unit

Equations

• Lean.Elab.Term.synthesizeSyntheticMVarsUsingDefault = do Lean.Elab.Term.synthesizeSyntheticMVars true false Lean.Elab.Term.synthesizeUsingDefaultLoop

@[inline]

def Lean.Elab.Term.withSynthesize {m : Type → Type u_1} {α : Type} [MonadFunctorT Lean.Elab.TermElabM m] [Monad m] (k : m α) (mayPostpone : optParam Bool false) : 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

• Lean.Elab.Term.withSynthesize k mayPostpone = monadMap (fun {β} x => Lean.Elab.Term.withSynthesizeImp x mayPostpone true) k

@[inline]

def Lean.Elab.Term.withSynthesizeLight {m : Type → Type u_1} {α : Type} [MonadFunctorT Lean.Elab.TermElabM m] [Monad m] (k : m α) : m α

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

Equations

• Lean.Elab.Term.withSynthesizeLight k = monadMap (fun {β} x => Lean.Elab.Term.withSynthesizeImp x true false) k

def Lean.Elab.Term.elabTermAndSynthesize (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

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.

def Lean.Elab.Term.runPendingTacticsAt (e : Lean.Expr) : Lean.Elab.TermElabM Unit

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.