class Iris.BI.BIAffine (PROP : Type u_1) [BI PROP] : Prop

Require that a separation logic with the carrier type PROP is an affine separation logic.

• affine (P : PROP) : Affine P

class Iris.BI.BIPositive (PROP : Type u_1) [BI PROP] : Prop

• affinely_sep_l {P Q : PROP} : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q

class Iris.BI.BILoeb (PROP : Type u_1) [BI PROP] : Prop

• loeb_weak {P : PROP} : (later P ⊢ P) → True ⊢ P

class Iris.BI.BILaterContractive (PROP : Type u_1) [BI PROP] extends Iris.OFE.Contractive Iris.BI.later : Prop

• distLater_dist {n : Nat} {x y : PROP} : DistLater n x y → Dist n (BI.later x) (BI.later y)

class Iris.BI.BIPersistentlyForall (PROP : Type u_1) [BI PROP] : Prop

• persistently_sForall_2 (Ψ : PROP → Prop) : («forall» fun (p : PROP) => iprop(⌜Ψ p⌝ → <pers> p)) ⊢ <pers> sForall Ψ