Mutable

structure Mutable (α : Type u) : Type u

• __mk__ :: (
• __get__ : α
• )

@[extern lean_mk_Mutable]

def Mutable.mk {α : Type u} (a : α) : Mutable α

Equations

• Mutable.mk a = { __get__ := a }

@[extern lean_Mutable_get]

def Mutable.get {α : Type u} (a : Mutable α) : α

Equations

• a.get = Mutable.__get__✝ a

theorem Mutable.ext {α : Type u} {x y : Mutable α} (get : x.get = y.get) : x = y

theorem Mutable.ext_iff {α : Type u} {x y : Mutable α} : x = y ↔ x.get = y.get

@[simp]

theorem Mutable.mk_eq_mk {α : Type u} {x y : α} : mk x = mk y ↔ x = y

@[extern lean_Mutable_modify]

unsafe def Mutable.getModifyUnsafe {α : Type u} (x : Mutable α) (f : α → α) : α

Equations

• x.getModifyUnsafe f = x.get

@[reducible, inline]

unsafe abbrev Mutable.getModifyImpl {α : Type u} (x : Mutable α) (f : α → α) (hf : ∀ (a : α), f a = a) : α

Equations

• x.getModifyImpl f hf = x.getModifyUnsafe f

@[implemented_by Mutable.getModifyImpl]

def Mutable.getModify {α : Type u} (x : Mutable α) (f : α → α) (hf : ∀ (a : α), f a = a) : α

Equations

• x.getModify f hf = f x.get

@[extern lean_Mutable_modify2]

unsafe def Mutable.getModify₂Unsafe {α : Type u} {β : Type v} (x : Mutable α) (f : α → β × α) : β

Equations

• x.getModify₂Unsafe f = (f x.get).fst

@[reducible, inline]

unsafe abbrev Mutable.getModify₂Impl {α : Type u} {β : Type v} (x : Mutable α) (f : α → β × α) (hgf : ∀ (a : α), (f a).snd = a) : β

Equations

• x.getModify₂Impl f hgf = x.getModify₂Unsafe f

@[implemented_by Mutable.getModify₂Impl]

def Mutable.getModify₂ {α : Type u} {β : Type v} (x : Mutable α) (f : α → β × α) (hgf : ∀ (a : α), (f a).snd = a) : β

Equations

• x.getModify₂ f hgf = (f x.get).fst