gcongrDischarger

Mathlib.Tactic.GCongr.Core

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

Lean4

/-- This is used as the default side-goal discharger,
it calls the `gcongr_discharger` extensible tactic.
-/
def gcongrDischarger (goal : MVarId) : MetaM Unit :=
  Elab.Term.TermElabM.run'
    (do
      trace[Meta.gcongr]"Attempting to discharge side goal {goal}"
      let [] ← Elab.Tactic.run goal <| Elab.Tactic.evalTactic (Unhygienic.run `(tactic| gcongr_discharger)) |
        failure)

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

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

Разделы

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

Аффилиация

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