elaboratePattern

Mathlib.Tactic.TermCongr

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

Lean4

/-- Given the pattern `t` in `congr(t)`, elaborate it for the given side
by replacing antiquotations with `cHole%` terms, and ensure the elaborated term
is of the expected type. -/
def elaboratePattern (t : Term) (expectedType? : Option Expr) (forLhs : Bool) : Term.TermElabM Expr :=
  Term.withoutErrToSorry do
    let t' ← processAntiquot t (fun h => if forLhs then `(cHole% lhs$h) else `(cHole% rhs$h))
    Term.elabTermEnsuringType t' expectedType?

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

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

Разделы

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

Аффилиация

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