def Iris.ProofMode.Replaces {PROP : Type u_1} [BI PROP] (K A B : PROP) : Prop

Equations

• Iris.ProofMode.Replaces K A B = ((B -∗ K) ⊢ A -∗ K)

theorem Iris.ProofMode.replaces_r {PROP : Type u_1} [BI PROP] {K P Q Q' : PROP} (h : Replaces K Q Q') : Replaces K iprop(P ∗ Q) iprop(P ∗ Q')

theorem Iris.ProofMode.replaces_l {PROP : Type u_1} [BI PROP] {K P P' Q : PROP} (h : Replaces K P P') : Replaces K iprop(P ∗ Q) iprop(P' ∗ Q)

theorem Iris.ProofMode.Replaces.apply {PROP : Type u_1} [BI PROP] {P P' Q : PROP} (h : Replaces Q P P') (h_entails : P' ⊢ Q) : P ⊢ Q

inductive Iris.ProofMode.ReplaceHyp {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (Q : Q(«$prop»)) : Type

• none {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {Q : Q(«$prop»)} : ReplaceHyp bi Q
• unchanged {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {Q : Q(«$prop»)} (ehyps' : Q(«$prop»)) (hyps' : Hyps bi ehyps') : ReplaceHyp bi Q
• main {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {Q : Q(«$prop»)} (e e' : Q(«$prop»)) (hyps' : Hyps bi e') (pf : Q(Replaces «$Q» «$e» «$e'»)) : ReplaceHyp bi Q

def Iris.ProofMode.Hyps.replace {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (Q : Q(«$prop»)) (uniq : Lean.Name) (repl : Lean.Name → Q(Bool) → Q(«$prop») → Lean.MetaM (ReplaceHyp bi Q)) {e : Q(«$prop»)} : Hyps bi e → Lean.MetaM (ReplaceHyp bi Q)

Equations

• One or more equations did not get rendered due to their size.
• Iris.ProofMode.Hyps.replace bi Q uniq repl (Iris.ProofMode.Hyps.emp x_3) = pure Iris.ProofMode.ReplaceHyp.none

theorem Iris.ProofMode.to_persistent_spatial {PROP : Type u_1} [BI PROP] {P P' Q : PROP} [hP : IntoPersistently false P P'] [or : Std.TCOr (BI.Affine P) (BI.Absorbing Q)] : Replaces Q P iprop(□ P')

theorem Iris.ProofMode.to_persistent_intuitionistic {PROP : Type u_1} [BI PROP] {P P' Q : PROP} [hP : IntoPersistently true P P'] : Replaces Q iprop(□ P) iprop(□ P')

def Iris.ProofMode.tacticIintuitionistic__ : Lean.ParserDescr

Equations

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

theorem Iris.ProofMode.from_affine {PROP : Type u_1} [BI PROP] {p : Bool} {P P' Q : PROP} [hP : FromAffinely P' P p] : Replaces Q iprop(□?p P) P'

def Iris.ProofMode.tacticIspatial__ : Lean.ParserDescr

Equations

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