withAdd

Mathlib.Tactic.ITauto

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.ITauto.Context.withAdd

Lean4

/-- Add `A` to the context `Γ` with proof `p`. This version of `Context.add` takes a continuation
and a target proposition `B`, so that in the case that `⊥` is found we can skip the continuation
and just prove `B` outright. -/
@[inline]
def withAdd (Γ : Context) (A : IProp) (p : Proof) (B : IProp) (f : Context → IProp → StateM Nat (Bool × Proof)) :
    StateM Nat (Bool × Proof) :=
  match Γ.add A p with
  | .ok Γ_A => f Γ_A B
  | .error p => pure (true, p B)

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

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

Разделы

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

Аффилиация

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