inductive Concurrency.MVar.State (a : Type) : Type

• empty {a : Type} : State a
• full {a : Type} : a → State a

instance Concurrency.MVar.instReprState {a✝ : Type} [Repr a✝] : Repr (State a✝)

Equations

• Concurrency.MVar.instReprState = { reprPrec := Concurrency.MVar.reprState✝ }

instance Concurrency.MVar.instDecidableEqState {a✝ : Type} [DecidableEq a✝] : DecidableEq (State a✝)

Equations

• Concurrency.MVar.instDecidableEqState = Concurrency.MVar.decEqState✝

instance Concurrency.MVar.instBEqState {a✝ : Type} [BEq a✝] : BEq (State a✝)

Equations

• Concurrency.MVar.instBEqState = { beq := Concurrency.MVar.beqState✝ }

def Concurrency.MVar.State.isEmpty {a : Type} : State a → Bool

Equations

• Concurrency.MVar.State.empty.isEmpty = true
• (Concurrency.MVar.State.full a_1).isEmpty = false

@[simp]

theorem Concurrency.MVar.State.isEmpty_empty {a : Type} : empty.isEmpty = true

@[simp]

theorem Concurrency.MVar.State.isEmpty_full {a✝ : Type} {a : a✝} : (full a).isEmpty = false

def Concurrency.MVar.State.isFull {a : Type} : State a → Bool

Equations

• Concurrency.MVar.State.empty.isFull = false
• (Concurrency.MVar.State.full a_1).isFull = true

@[simp]

theorem Concurrency.MVar.State.isFull_empty {a : Type} : empty.isFull = false

@[simp]

theorem Concurrency.MVar.State.isFull_full {a✝ : Type} {a : a✝} : (full a).isFull = true

def Concurrency.MVar.State.get? {a : Type} (self : State a) : Option a

Equations

• Concurrency.MVar.State.empty.get? = none
• (Concurrency.MVar.State.full a_1).get? = some a_1

def Concurrency.MVar.State.get {a : Type} (self : State a) : self.isFull = true → a

Equations

• (Concurrency.MVar.State.full x_2).get x_3 = x_2