elabPatterns

Mathlib.Tactic.CasesM

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.elabPatterns

Lean4

/-- Elaborate a list of terms with holes into a list of patterns. -/
def elabPatterns (pats : Array Term) : TermElabM (Array AbstractMVarsResult) :=
  withTheReader Term.Context (fun ctx ↦ { ctx with ignoreTCFailures := true }) <|
    Term.withoutErrToSorry <|
      pats.mapM fun p ↦
        Term.withoutModifyingElabMetaStateWithInfo do
          withRef p <| abstractMVars (← Term.elabTerm p none)

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

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

Разделы

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

Аффилиация

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