class Iris.BI.Persistent {PROP : Type u_1} [BI PROP] (P : PROP) : Prop

Require that the proposition P is persistent.

• persistent : P ⊢ <pers> P

class Iris.BI.Affine {PROP : Type u_1} [BI PROP] (P : PROP) : Prop

Require that the proposition P is affine.

• affine : P ⊢ emp

class Iris.BI.Absorbing {PROP : Type u_1} [BI PROP] (P : PROP) : Prop

Require that the proposition P is absorbing.

• absorbing : <absorb> P ⊢ P

class Iris.BI.Intuitionistic {PROP : Type u_1} [BI PROP] (P : PROP) : Prop

Require that the proposition P is intuitionistic.

• intuitionistic : P ⊢ □ P

class Iris.BI.Timeless {PROP : Type u_1} [BI PROP] (P : PROP) : Prop

Require that the proposition P does not depend on the step index

• timeless : ⊢ later P ∨ ◇ P