Documentation

Lean.Elab.SyntheticMVars

partial def Lean.Elab.Term.runTactic (mvarId : Lean.MVarId) (tacticCode : Lean.Syntax) :

Lean.Elab.TermElabM Unit

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

Lean.Elab.TermElabM Unit

partial def Lean.Elab.Term.synthesizeSyntheticMVars.loop (mayPostpone : optParam Bool true) (ignoreStuckTC : optParam Bool false) (u : 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} [inst : MonadFunctorT Lean.Elab.TermElabM m] [inst : Monad m] (k : m α) (mayPostpone : optParam Bool false) :

m α

Equations

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

@[inline]

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

m α

Equations

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

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

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.elabTermAndSynthesize stx expectedType? = Lean.withRef stx do let a ← Lean.Elab.Term.withSynthesize (Lean.Elab.Term.elabTerm stx expectedType? true true) liftM (Lean.Meta.instantiateMVars a)