A map that keeps insertion order

Setting a present key replaces its value in place; setting a new key appends it; erasing keeps the order of the rest.

structure Cryptlib.Protocols.GroupComm.Common.Dict (K V : Type) : Type

• pairs : List (K × V)

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.Common.instInhabitedDict {a✝ a✝¹ : Type} : Inhabited (Dict a✝ a✝¹)

Equations

• Cryptlib.Protocols.GroupComm.Common.instInhabitedDict = { default := Cryptlib.Protocols.GroupComm.Common.instInhabitedDict.default }

def Cryptlib.Protocols.GroupComm.Common.instDecidableEqDict.decEq {K✝ V✝ : Type} [DecidableEq K✝] [DecidableEq V✝] (x✝ x✝¹ : Dict K✝ V✝) : Decidable (x✝ = x✝¹)

Equations

• Cryptlib.Protocols.GroupComm.Common.instDecidableEqDict.decEq { pairs := a } { pairs := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.Common.instDecidableEqDict {K✝ V✝ : Type} [DecidableEq K✝] [DecidableEq V✝] : DecidableEq (Dict K✝ V✝)

Equations

• Cryptlib.Protocols.GroupComm.Common.instDecidableEqDict = Cryptlib.Protocols.GroupComm.Common.instDecidableEqDict.decEq

def Cryptlib.Protocols.GroupComm.Common.Dict.empty {K V : Type} : Dict K V

Equations

• Cryptlib.Protocols.GroupComm.Common.Dict.empty = { pairs := [] }

@[instance_reducible]

instance Cryptlib.Protocols.GroupComm.Common.Dict.instEmptyCollection {K V : Type} : EmptyCollection (Dict K V)

Equations

• Cryptlib.Protocols.GroupComm.Common.Dict.instEmptyCollection = { emptyCollection := Cryptlib.Protocols.GroupComm.Common.Dict.empty }

def Cryptlib.Protocols.GroupComm.Common.Dict.get? {K V : Type} [DecidableEq K] (d : Dict K V) (k : K) : Option V

Equations

• d.get? k = Option.map (fun (x : K × V) => x.snd) (List.find? (fun (x : K × V) => decide (x.fst = k)) d.pairs)

def Cryptlib.Protocols.GroupComm.Common.Dict.getD {K V : Type} [DecidableEq K] (d : Dict K V) (k : K) (v : V) : V

Equations

• d.getD k v = (d.get? k).getD v

def Cryptlib.Protocols.GroupComm.Common.Dict.contains {K V : Type} [DecidableEq K] (d : Dict K V) (k : K) : Bool

Equations

• d.contains k = (d.get? k).isSome

def Cryptlib.Protocols.GroupComm.Common.Dict.set {K V : Type} [DecidableEq K] (d : Dict K V) (k : K) (v : V) : Dict K V

Equations

• d.set k v = if d.contains k = true then { pairs := List.map (fun (p : K × V) => if p.fst = k then (k, v) else p) d.pairs } else { pairs := d.pairs ++ [(k, v)] }

def Cryptlib.Protocols.GroupComm.Common.Dict.setDefault {K V : Type} [DecidableEq K] (d : Dict K V) (k : K) (v : V) : Dict K V

Set k only if it is absent.

Equations

• d.setDefault k v = if d.contains k = true then d else d.set k v

def Cryptlib.Protocols.GroupComm.Common.Dict.modify {K V : Type} [DecidableEq K] (d : Dict K V) (k : K) (f : V → V) : Dict K V

Equations

• d.modify k f = match d.get? k with | some v => d.set k (f v) | none => d

def Cryptlib.Protocols.GroupComm.Common.Dict.erase {K V : Type} [DecidableEq K] (d : Dict K V) (k : K) : Dict K V

Equations

• d.erase k = { pairs := List.filter (fun (x : K × V) => decide (x.fst ≠ k)) d.pairs }

def Cryptlib.Protocols.GroupComm.Common.Dict.keys {K V : Type} (d : Dict K V) : List K

Equations

• d.keys = List.map (fun (x : K × V) => x.fst) d.pairs

def Cryptlib.Protocols.GroupComm.Common.Dict.values {K V : Type} (d : Dict K V) : List V

Equations

• d.values = List.map (fun (x : K × V) => x.snd) d.pairs

def Cryptlib.Protocols.GroupComm.Common.Dict.size {K V : Type} (d : Dict K V) : Nat

Equations

• d.size = d.pairs.length

def Cryptlib.Protocols.GroupComm.Common.Dict.filter {K V : Type} (d : Dict K V) (p : K → V → Bool) : Dict K V

Equations

• d.filter p = { pairs := List.filter (fun (e : K × V) => p e.fst e.snd) d.pairs }

def Cryptlib.Protocols.GroupComm.Common.Dict.mapValues {K V W : Type} (d : Dict K V) (f : V → W) : Dict K W

Equations

• d.mapValues f = { pairs := List.map (fun (e : K × V) => (e.fst, f e.snd)) d.pairs }

def Cryptlib.Protocols.GroupComm.Common.Dict.mapWithKey {K V W : Type} (d : Dict K V) (f : K → V → W) : Dict K W

Equations

• d.mapWithKey f = { pairs := List.map (fun (e : K × V) => (e.fst, f e.fst e.snd)) d.pairs }

def Cryptlib.Protocols.GroupComm.Common.Dict.ofList {K V : Type} [DecidableEq K] (l : List (K × V)) : Dict K V

Build a map from pairs in order; a later value for a key replaces an earlier one in place.

Equations

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