theorem Iris.ProofMode.clear_spatial {PROP : Type u_1} [BI PROP] {P P' A Q : PROP} [Std.TCOr (BI.Affine A) (BI.Absorbing Q)] (h_rem : P ⊣⊢ P' ∗ A) (h : P' ⊢ Q) : P ⊢ Q

theorem Iris.ProofMode.clear_intuitionistic {PROP : Type u_1} [BI PROP] {P P' A Q : PROP} (h_rem : P ⊣⊢ P' ∗ □ A) (h : P' ⊢ Q) : P ⊢ Q

def Iris.ProofMode.clearCore {u : Lean.Level} {prop : Q(Type u)} (_bi : Q(BI «$prop»)) (e e' out goal : Q(«$prop»)) (pf : Q(«$e» ⊣⊢ «$e'» ∗ «$out»)) : Lean.MetaM Q((«$e'» ⊢ «$goal») → «$e» ⊢ «$goal»)

Equations

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

def Iris.ProofMode.tacticIclear__ : Lean.ParserDescr

Equations

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