Documentation

Lean.Elab.SyntheticMVars

source
def Lean.Elab.Term.reportStuckSyntheticMVar (mvarSyntheticDecl : Lean.Elab.Term.SyntheticMVarDecl) (ignoreStuckTC : optParam Bool false) :
Lean.Elab.TermElabM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Elab.Term.runTactic (mvarId : Lean.MVarId) (tacticCode : Lean.Syntax) :
Lean.Elab.TermElabM Unit
source
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 syntheticMVars 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.
source
partial def Lean.Elab.Term.synthesizeSyntheticMVars.loop (mayPostpone : optParam Bool true) (ignoreStuckTC : optParam Bool false) :
Unit → Lean.Elab.TermElabM Unit
source
def Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC : optParam Bool false) :
Lean.Elab.TermElabM Unit
Equations
source
def Lean.Elab.Term.synthesizeSyntheticMVarsUsingDefault:
Lean.Elab.TermElabM Unit
Equations
source
@[inline]
def Lean.Elab.Term.withSynthesize {m : Type → Type u_1} {α : Type} [inst : MonadFunctorT Lean.Elab.TermElabM m] [inst : 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
source
@[inline]
def Lean.Elab.Term.withSynthesizeLight {m : Type → Type u_1} {α : Type} [inst : MonadFunctorT Lean.Elab.TermElabM m] [inst : Monad m] (k : m α) :
m α

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

Equations
source
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.