Mutable

opaque MutableAux (α : Type u) : { x : Type u // x = α }

def Mutable (α : Type u) : Type u

Equations

• Mutable α = (MutableAux α).val

@[extern lean_st_mk_ref]

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

Equations

• Mutable.mk a = ⋯.mpr a

@[never_extract, extern lean_st_ref_get]

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

Equations

• x.get = ⋯.mp x

@[never_extract, extern lean_Mutable_set]

unsafe def Mutable.set {α : Type u} {β : Type v} (x : Mutable α) (a : α) (b : β) : β

Equations

• x.set a b = b

@[simp]

theorem Mutable.mk_get {α : Type u} (x : Mutable α) : mk x.get = x

@[simp]

theorem Mutable.get_mk {α : Type u} (x : α) : (mk x).get = x

def Mutable.rec {α : Type u} {motive : Mutable α → Sort u_1} (h : (a : α) → motive (mk a)) (x : Mutable α) : motive x

Equations

• Mutable.rec h x = ⋯ ▸ h x.get

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_inj {α : Type u} {x y : α} : mk x = mk y ↔ x = y

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

Equations

• x.modifyUnsafe f = x.set (f x.get) (f x.get)

@[reducible, inline]

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

Equations

• x.modifyImpl f hf = x.modifyUnsafe f

@[implemented_by Mutable.modifyImpl]

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

Equations

• x.modify f hf = f x.get

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

Equations

• x.getModifyUnsafe f = match f x.get with | (b, a) => x.set a b

@[reducible, inline]

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

Equations

• x.getModifyImpl f hgf = x.getModifyUnsafe f

@[implemented_by Mutable.getModifyImpl]

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

@[simp]

theorem Mutable.getModify_mk {α : Type u} {β : Type v} {a : α} {f : α → β × α} {hgf : ∀ (a : α), (f a).snd = a} : (mk a).getModify f hgf = (f a).fst