elabPattern

Mathlib.Lean.Elab.Term

URI: https://scilib.ai/kg/mathlib#Lean.Elab.Term.elabPattern

Lean4

/-- Fully elaborates the term `patt`, allowing typeclass inference failure,
but while setting `errToSorry` to false.
Typeclass failures result in plain metavariables.
Instantiates all assigned metavariables. -/
def elabPattern (patt : Term) (expectedType? : Option Expr) : TermElabM Expr := do
  withTheReader Term.Context ({ · with ignoreTCFailures := true, errToSorry := false }) <|
      withSynthesizeLight do
        let t ← elabTerm patt expectedType?
        synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
        instantiateMVars t

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru