Additional functionality for KVMap

ink

def Lean.KVMap.eraseCore : List (Lean.Name × Lean.DataValue) → Lean.Name → List (Lean.Name × Lean.DataValue)

erase pairs whose names match the second argument from a list of Name × DataValue pairs

Equations

• Lean.KVMap.eraseCore x x = match x, x with | l, n => List.filter (fun a => decide (a.fst ≠ n)) l

ink

def Lean.KVMap.erase : Lean.KVMap → Lean.Name → Lean.KVMap

erase an entry from the map

Equations

• Lean.KVMap.erase x x = match x, x with | { entries := m }, k => { entries := Lean.KVMap.eraseCore m k }

ink

def Lean.KVMap.updateBool (m : Lean.KVMap) (k : Lean.Name) (f : Bool → Bool) : Lean.KVMap

update a Boolean entry based on its current value.

Equations

• Lean.KVMap.updateBool m k f = Lean.KVMap.insert m k (Lean.DataValue.ofBool (f (Lean.KVMap.getBool m k)))