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.

inductive Lean.Elab.Term.PostponeBehavior : Type

Auxiliary type for synthesizeSyntheticMVars. It specifies whether pending synthetic metavariables can be postponed or not.

• yes: Lean.Elab.Term.PostponeBehavior

  Any kind of pending synthetic metavariable can be postponed. Universe constrains may also be postponed.

• no: Lean.Elab.Term.PostponeBehavior

  Pending synthetic metavariables cannot be postponed.

• partial: Lean.Elab.Term.PostponeBehavior

  Synthectic metavariables associated with type class resolution can be postponed. Motivation: this kind of metavariable are not synthethic opaque, and can be assigned by isDefEq. Unviverse constraints can also be postponed.

instance Lean.Elab.Term.instInhabitedPostponeBehavior : Inhabited Lean.Elab.Term.PostponeBehavior

Equations

• Lean.Elab.Term.instInhabitedPostponeBehavior = { default := Lean.Elab.Term.PostponeBehavior.yes }

instance Lean.Elab.Term.instReprPostponeBehavior : Repr Lean.Elab.Term.PostponeBehavior

Equations

• Lean.Elab.Term.instReprPostponeBehavior = { reprPrec := Lean.Elab.Term.reprPostponeBehavior✝ }

instance Lean.Elab.Term.instBEqPostponeBehavior : BEq Lean.Elab.Term.PostponeBehavior

Equations

• Lean.Elab.Term.instBEqPostponeBehavior = { beq := Lean.Elab.Term.beqPostponeBehavior✝ }

def Lean.Elab.Term.PostponeBehavior.ofBool : Bool → Lean.Elab.Term.PostponeBehavior

Equations

• Lean.Elab.Term.PostponeBehavior.ofBool true = Lean.Elab.Term.PostponeBehavior.yes
• Lean.Elab.Term.PostponeBehavior.ofBool false = Lean.Elab.Term.PostponeBehavior.no

partial def Lean.Elab.Term.runTactic (mvarId : Lean.MVarId) (tacticCode : Lean.Syntax) (report : optParam Bool true) : Lean.Elab.TermElabM Unit

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

The tacticCode syntax comprises the whole by ... expression.

If report := false, then runTactic will not capture exceptions nor will report unsolved goals. Unsolved goals become exceptions.

partial def Lean.Elab.Term.synthesizeSyntheticMVars (postpone : optParam Lean.Elab.Term.PostponeBehavior Lean.Elab.Term.PostponeBehavior.yes) (ignoreStuckTC : optParam Bool false) : Lean.Elab.TermElabM Unit

Try to process pending synthetic metavariables.

If postpone == .no,then pendingMVars is [] after executing this method. If postpone == .partial, then pendingMVars contains only .tc and .coe kinds.

It keeps executing synthesizeSyntheticMVarsStep while progress is being made. If postpone != .yes, then it applies default instances to SyntheticMVarKind.typeClass (if available) metavariables that are still unresolved, and then tries to resolve metavariables with postponeOnError == 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 If postpone == .no.

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 (postpone : optParam Lean.Elab.Term.PostponeBehavior Lean.Elab.Term.PostponeBehavior.yes) (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 Lean.Elab.Term.PostponeBehavior.no ignoreStuckTC

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

Equations

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

@[inline]

def Lean.Elab.Term.withSynthesize {m : Type → Type u_1} {α : Type} [MonadFunctorT Lean.Elab.TermElabM m] (k : m α) (postpone : optParam Lean.Elab.Term.PostponeBehavior Lean.Elab.Term.PostponeBehavior.no) : 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 postpone = monadMap (fun {β : Type} (x : Lean.Elab.TermElabM β) => Lean.Elab.Term.withSynthesizeImp x postpone) k

@[inline]

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

Similar to withSynthesize, but uses postpone := .true, does not use use synthesizeUsingDefault

Equations

• Lean.Elab.Term.withSynthesizeLight k = monadMap (fun {β : Type} (x : Lean.Elab.TermElabM β) => Lean.Elab.Term.withSynthesizeLightImp x) 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.