@[reducible, inline]

abbrev Iris.Instances.Classical.HeapProp (Val : Type u_1) : Type u_1

Equations

• Iris.Instances.Classical.HeapProp Val = (Iris.Instances.Data.State Val → Prop)

instance Iris.Instances.Classical.instBIBaseHeapProp {Val : Type u_1} : BI.BIBase (HeapProp Val)

Equations

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

instance Iris.Instances.Classical.instPreorderHeapPropEntails {Val : Type u_1} : Std.Preorder BI.Entails

instance Iris.Instances.Classical.instCOFEHeapProp {Val : Type u_1} : COFE (HeapProp Val)

Equations

• Iris.Instances.Classical.instCOFEHeapProp = Iris.COFE.ofDiscrete Eq ⋯

instance Iris.Instances.Classical.instBIHeapProp {Val : Type u_1} : BI (HeapProp Val)

Equations

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