inductive Iris.Instances.Data.StateResult (α : Type u_1) : Type u_1

Result of an operation on State.

• unknown {α : Type u_1} : StateResult α
• result {α : Type u_1} (x : α) : StateResult α
• conflict {α : Type u_1} : StateResult α

@[reducible, inline]

abbrev Iris.Instances.Data.State (Val : Type u_1) : Type u_1

Implementation of a state datatype as a map from Nat to a StateResult with a value from Val.

Equations

• Iris.Instances.Data.State Val = (Nat → Iris.Instances.Data.StateResult Val)

instance Iris.Instances.Data.instEmptyCollectionState {Val : Type u_1} : EmptyCollection (State Val)

Equations

• Iris.Instances.Data.instEmptyCollectionState = { emptyCollection := fun (x : Nat) => Iris.Instances.Data.unknown }

instance Iris.Instances.Data.instHasSubsetState {Val : Type u_1} : HasSubset (State Val)

Equations

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

instance Iris.Instances.Data.instUnionState {Val : Type u_1} : Union (State Val)

Equations

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

instance Iris.Instances.Data.instDisjointState {Val : Type u_1} : Disjoint (State Val)

Equations

• Iris.Instances.Data.instDisjointState = { disjoint := fun (a b : Iris.Instances.Data.State Val) => ∀ (i : Nat), a i = Iris.Instances.Data.unknown ∨ b i = Iris.Instances.Data.unknown }

theorem Iris.Instances.Data.empty_union {Val : Type u_1} {s : State Val} : s = ∅ ∪ s

theorem Iris.Instances.Data.union_comm {Val : Type u_1} {a b : State Val} : a ∪ b = b ∪ a

theorem Iris.Instances.Data.union_assoc {Val : Type u_1} {a b c : State Val} : a ∪ b ∪ c = a ∪ (b ∪ c)

theorem Iris.Instances.Data.empty_disjoint {Val : Type u_1} {s : State Val} : ∅ || s

theorem Iris.Instances.Data.disjoint_comm {Val : Type u_1} {a b : State Val} : a || b ↔ b || a

theorem Iris.Instances.Data.disjoint_assoc {Val : Type u_1} {a b c : State Val} : a ∪ b || c → a || b → a || c ∧ b || c

theorem Iris.Instances.Data.disjoint_union {Val : Type u_1} {a b c : State Val} : a || b → a || c → a || b ∪ c