gcongrForwardDischarger

Mathlib.Tactic.GCongr.Core

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

Lean4

/-- This is used as the default main-goal discharger,
consisting of running `Lean.MVarId.gcongrForward` (trying a term together with limited
forward-reasoning on that term) on each nontrivial hypothesis.
-/
def gcongrForwardDischarger (goal : MVarId) : MetaM Unit :=
  Elab.Term.TermElabM.run' do
    let mut hs :=
      #[]
        -- collect the nontrivial hypotheses

    for h in ← getLCtx do
      if !h.isImplementationDetail then
        hs :=
          hs.push
            (.fvar h.fvarId)
              -- run `Lean.MVarId.gcongrForward` on each one

    goal.gcongrForward hs

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

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

Разделы

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

Аффилиация

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