processAntiquot

Mathlib.Tactic.TermCongr

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

Lean4

/-- Replace all `term` antiquotations in a term using the given `expand` function. -/
def processAntiquot (t : Term) (expand : Term → Term.TermElabM Term) : Term.TermElabM Term := do
  let t' ←
    t.raw.replaceM fun s => do
        if s.isAntiquots then
          let ks := s.antiquotKinds
          unless ks.any (fun (k, _) => k == `term) do
            throwErrorAt s "Expecting term"
          let h : Term := ⟨s.getCanonicalAntiquot.getAntiquotTerm⟩
          expand h
        else
          pure none
  return ⟨t'⟩

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

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

Разделы

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

Аффилиация

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