structure Iris.ProofMode.SpecializeState {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (orig : Q(«$prop»)) : Type

• e : Q(«$prop»)
• hyps : Hyps bi self.e
• b : Q(Bool)
• out : Q(«$prop»)
• pf : Q(«$orig» ⊢ unknown_1 ∗ □?unknown_2 unknown_3)

theorem Iris.ProofMode.specialize_wand {PROP : Type u_1} [BI PROP] {q p : Bool} {A1 A2 A3 Q P1 P2 : PROP} (h1 : A1 ⊢ A2 ∗ □?q Q) (h2 : A2 ⊣⊢ A3 ∗ □?p P1) [inst : IntoWand q p Q P1 P2] : A1 ⊢ A3 ∗ □?(p && q) P2

theorem Iris.ProofMode.specialize_forall {PROP : Type u_1} [BI PROP] {p : Bool} {A1 A2 P : PROP} {α : Sort u_2} {Φ : α → PROP} [inst : IntoForall P Φ] (h : A1 ⊢ A2 ∗ □?p P) (a : α) : A1 ⊢ A2 ∗ □?p Φ a

def Iris.ProofMode.SpecializeState.process1 {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {orig : Q(«$prop»)} : SpecializeState bi orig → Lean.Term → Lean.Elab.TermElabM (SpecializeState bi orig)

Equations

• One or more equations did not get rendered due to their size.

def Iris.ProofMode.tacticIspecialize___As_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Iris.ProofMode.tacticIspecialize___ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.