existsi

Mathlib.Lean.Meta

URI: https://scilib.ai/kg/mathlib#Lean.MVarId.existsi

Lean4

/-- Has the effect of `refine ⟨e₁,e₂,⋯, ?_⟩`.
-/
def existsi (mvar : MVarId) (es : List Expr) : MetaM MVarId := do
  es.foldlM
      (fun mv e ↦ do
        let (subgoals, _) ←
          Elab.Term.TermElabM.run <|
              Elab.Tactic.run mv do
                Elab.Tactic.evalTactic (← `(tactic| refine ⟨?_, ?_⟩))
        let [sg1, sg2] := subgoals |
          throwError"expected two subgoals"
        sg1.assign e
        pure sg2)
      mvar

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

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

Разделы

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

Аффилиация

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