1.3. Dictionaries🔗

The Gray Paper's partial-function / dictionary type D⟨K, V⟩ is modeled as an association list.

structure

Dict (K V : Type) [BEq K] : Type
Dict (K V : Type) [BEq K] : Type

A dictionary ⟨K→V⟩ : partial mapping with enumerable key-value pairs. GP §3.5. Represented as sorted association list with unique keys.

Constructor

Dict.mk

Fields

entries : List (K × V)

def

Dict.empty {K V : Type} [BEq K] : Dict K V
Dict.empty {K V : Type} [BEq K] : Dict K V

def

Dict.lookup {K V : Type} [BEq K] (d : Dict K V) (k : K) : Option V
Dict.lookup {K V : Type} [BEq K]
  (d : Dict K V) (k : K) : Option V

Lookup: d[k]. GP §3.5.

def

Dict.insert {K V : Type} [BEq K] (d : Dict K V) (k : K) (v : V) :
  Dict K V
Dict.insert {K V : Type} [BEq K]
  (d : Dict K V) (k : K) (v : V) :
  Dict K V

Insert or update a key-value pair.

def

Dict.erase {K V : Type} [BEq K] (d : Dict K V) (k : K) : Dict K V
Dict.erase {K V : Type} [BEq K]
  (d : Dict K V) (k : K) : Dict K V

Remove a key from the dictionary.

def

Dict.size {K V : Type} [BEq K] (d : Dict K V) : Nat
Dict.size {K V : Type} [BEq K]
  (d : Dict K V) : Nat

Number of entries.

def

Dict.keys {K V : Type} [BEq K] (d : Dict K V) : List K
Dict.keys {K V : Type} [BEq K]
  (d : Dict K V) : List K

Domain: 𝒦(d). GP §3.5.

def

Dict.values {K V : Type} [BEq K] (d : Dict K V) : List V
Dict.values {K V : Type} [BEq K]
  (d : Dict K V) : List V

Range: 𝒱(d). GP §3.5.

def

Dict.subtract {K V : Type} [BEq K] (d : Dict K V) (ks : List K) :
  Dict K V
Dict.subtract {K V : Type} [BEq K]
  (d : Dict K V) (ks : List K) : Dict K V

Dictionary subtraction: d ∖ s. GP §3.5.

def

Dict.union {K V : Type} [BEq K] (d e : Dict K V) : Dict K V
Dict.union {K V : Type} [BEq K]
  (d e : Dict K V) : Dict K V

Dictionary union with right-bias: d ∪ e. GP §3.5.