class Iris.ProofMode.AsEmpValid1 (φ : outParam Prop) {PROP : Type u_1} (P : PROP) [BI PROP] : Prop

• as_emp_valid : φ ↔ ⊢ P

class Iris.ProofMode.AsEmpValid2 (φ : Prop) {PROP : outParam (Type u_1)} (P : outParam PROP) [BI PROP] : Prop

• as_emp_valid : φ ↔ ⊢ P

def Iris.ProofMode.AsEmpValid1.to2 {φ : Prop} {PROP : Type u_1} {P : PROP} [BI PROP] [AsEmpValid1 φ P] : AsEmpValid2 φ P

Equations

• ⋯ = ⋯

def Iris.ProofMode.AsEmpValid2.to1 {φ : Prop} {PROP : Type u_1} {P : PROP} [BI PROP] [AsEmpValid2 φ P] : AsEmpValid1 φ P

Equations

• ⋯ = ⋯

theorem Iris.ProofMode.as_emp_valid_1 {PROP : Type u_1} {φ : Prop} [BI PROP] (P : PROP) [AsEmpValid1 φ P] : φ → ⊢ P

theorem Iris.ProofMode.as_emp_valid_2 {PROP : Type u_1} {P : PROP} [BI PROP] (φ : Prop) [AsEmpValid2 φ P] : (⊢ P) → φ

class Iris.ProofMode.FromImp {PROP : Type u_1} [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) : Prop

• from_imp : (Q1 → Q2) ⊢ P

class Iris.ProofMode.FromWand {PROP : Type u_1} [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) : Prop

• from_wand : (Q1 -∗ Q2) ⊢ P

class Iris.ProofMode.IntoWand {PROP : Type u_1} [BI PROP] (p q : Bool) (R P : PROP) (Q : outParam PROP) : Prop

• into_wand : □?p R ⊢ □?q P -∗ Q

class Iris.ProofMode.FromForall {PROP : Type u_1} [BI PROP] (P : PROP) {α : outParam (Sort u_2)} (Ψ : outParam (α → PROP)) : Prop

• from_forall : (BI.forall fun (x : α) => Ψ x) ⊢ P

class Iris.ProofMode.IntoForall {PROP : Type u_1} [BI PROP] (P : PROP) {α : outParam (Sort u_2)} (Φ : outParam (α → PROP)) : Prop

• into_forall : P ⊢ BI.forall fun (x : α) => Φ x

class Iris.ProofMode.FromExists {PROP : Type u_1} [BI PROP] (P : PROP) {α : outParam (Sort u_2)} (Φ : outParam (α → PROP)) : Prop

• from_exists : (BI.exists fun (x : α) => Φ x) ⊢ P

class Iris.ProofMode.IntoExists {PROP : Type u_1} [BI PROP] (P : PROP) {α : outParam (Sort u_2)} (Φ : outParam (α → PROP)) : Prop

• into_exists : P ⊢ BI.exists fun (x : α) => Φ x

class Iris.ProofMode.FromAnd {PROP : Type u_1} [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) : Prop

• from_and : Q1 ∧ Q2 ⊢ P

class Iris.ProofMode.IntoAnd {PROP : Type u_1} (p : Bool) [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) : Prop

• into_and : □?p P ⊢ □?p (Q1 ∧ Q2)

class Iris.ProofMode.FromSep {PROP : Type u_1} [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) : Prop

• from_sep : Q1 ∗ Q2 ⊢ P

class Iris.ProofMode.IntoSep {PROP : Type u_1} [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) : Prop

• into_sep : P ⊢ Q1 ∗ Q2

class Iris.ProofMode.FromOr {PROP : Type u_1} [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) : Prop

• from_or : Q1 ∨ Q2 ⊢ P

class Iris.ProofMode.IntoOr {PROP : Type u_1} [BI PROP] (P : PROP) (Q1 Q2 : outParam PROP) : Prop

• into_or : P ⊢ Q1 ∨ Q2

class Iris.ProofMode.IntoPersistently {PROP : Type u_1} (p : Bool) [BI PROP] (P : PROP) (Q : outParam PROP) : Prop

• into_persistently : <pers>?p P ⊢ <pers> Q

class Iris.ProofMode.FromAffinely {PROP : Type u_1} [BI PROP] (P : outParam PROP) (Q : PROP) (p : Bool := true) : Prop

• from_affinely : <affine>?p Q ⊢ P

class Iris.ProofMode.IntoAbsorbingly {PROP : Type u_1} [BI PROP] (P : outParam PROP) (Q : PROP) : Prop

• into_absorbingly : P ⊢ <absorb> Q

class Iris.ProofMode.FromAssumption {PROP : Type u_1} (p : Bool) [BI PROP] (P Q : PROP) : Prop

• from_assumption : □?p P ⊢ Q

class Iris.ProofMode.IntoPure {PROP : Type u_1} [BI PROP] (P : PROP) (φ : outParam Prop) : Prop

• into_pure : P ⊢ ⌜φ⌝

class Iris.ProofMode.FromPure {PROP : Type u_1} [BI PROP] (a : outParam Bool) (P : PROP) (φ : outParam Prop) : Prop

• from_pure : <affine>?a ⌜φ⌝ ⊢ P