elabTermForConvert — Mathlib

Lean4
/-- Elaborates `term` ensuring the expected type, allowing stuck metavariables.
Returns stuck metavariables as additional goals.
-/
def elabTermForConvert (term : Syntax) (expectedType? : Option Expr) : TacticM (Expr × List MVarId) := do
  withCollectingNewGoalsFrom (parentTag := ← getMainTag) (tagSuffix := `convert) (allowNaturalHoles := true) do
      -- Allow typeclass inference failures since these will be inferred by unification
          -- or else become new goals

      withTheReader Term.Context (fun ctx => { ctx with ignoreTCFailures := true })
          (do
            let t ← elabTermEnsuringType (mayPostpone := true) term expectedType?
            Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
            return t)
Похожие утверждения