inductive TMap (α β : Type) : Type

Total map as recursive type with a key type α and value of type β. The empty map takes a default value d of type β.

• empty {α β : Type} (d : β) : TMap α β
• put {α β : Type} (k : α) (v : β) (t : TMap α β) : TMap α β

def instReprTMap.repr {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : TMap α✝ β✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance instReprTMap {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Repr (TMap α✝ β✝)

Equations

• instReprTMap = { reprPrec := instReprTMap.repr }

@[implicit_reducible]

instance instInhabitedTMap {a✝ a✝¹ : Type} [Inhabited a✝¹] : Inhabited (TMap a✝ a✝¹)

Equations

• instInhabitedTMap = { default := instInhabitedTMap.default }

def TMap.get {α : Type} [BEq α] [LawfulBEq α] {β : Type} (map : TMap α β) (k : α) : β

Let k ∈ α and v, d ∈ β. The function TMap.get(k) returns either the value v assigned to k or d as the default value if no assignment to k.

Equations

• (TMap.empty a).get k = a
• (a ↦ a_1; a_2).get k = if (k == a) = true then a_1 else a_2.get k

def TMap.getKeysAux {α β : Type} [BEq α] [LawfulBEq α] (map : TMap α β) (list : List α) : List α

Accumulate the keys of a TMap onto list, used by getKeys.

Equations

• (TMap.empty a).getKeysAux list = list
• (a ↦ a_1; a_2).getKeysAux list = a_2.getKeysAux (a :: list)

def TMap.getKeys {α β : Type} [BEq α] [LawfulBEq α] (map : TMap α β) : List α

Get all keys of a map as a list

Equations

• map.getKeys = map.getKeysAux []

def TMap.getLastKey {α β : Type} [BEq α] [LawfulBEq α] (map : TMap α β) : Option α

The most recently inserted key of a TMap, if any.

Equations

• map.getLastKey = match map.getKeys.reverse with | v :: tail => some v | x => none

def TMap.getValuesAux {α β : Type} [BEq α] [LawfulBEq α] (map : TMap α β) (list : List β) : List β

Accumulate the values of a TMap onto list, used by getValues.

Equations

• (TMap.empty a).getValuesAux list = list
• (a ↦ a_1; a_2).getValuesAux list = a_2.getValuesAux (a_1 :: list)

def TMap.getValues {α β : Type} [BEq α] [LawfulBEq α] (map : TMap α β) : List β

Get all values of a map as a list

Equations

• map.getValues = map.getValuesAux []

def TMap.toStringAux {α β : Type} [ToString α] [ToString β] (t : TMap α β) : String

Render the bindings of a TMap as a ; -separated string, used by toString.

Equations

• (TMap.empty a).toStringAux = toString a
• (a ↦ a_1; a_2).toStringAux = toString a ++ toString " ↦ " ++ toString a_1 ++ toString "; " ++ a_2.toStringAux ++ ""

def TMap.toString {α β : Type} [ToString α] [ToString β] (t : TMap α β) : String

Render a TMap as a parenthesised string of its bindings.

Equations

• t.toString = "(" ++ t.toStringAux ++ ")"

@[implicit_reducible]

instance instReprTMapOfToString {α β : Type} [ToString α] [ToString β] : Repr (TMap α β)

Equations

• instReprTMapOfToString = { reprPrec := fun (t : TMap α β) (x : Nat) => Std.Format.text t.toString }

def «term(_↦_;_)» : Lean.ParserDescr

Notation (k ↦ v; m) for inserting the binding k ↦ v into the total map m.

Equations

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

inductive PMap (α β : Type) : Type

Partial map as recursive type with a key type α and value of type β is defined. Returns an option.

• empty {α β : Type} : PMap α β
• put {α β : Type} (k : α) (v : β) (t : PMap α β) : PMap α β

def instReprPMap.repr {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : PMap α✝ β✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprPMap.repr PMap.empty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PMap.empty")).group prec✝

@[implicit_reducible]

instance instReprPMap {α✝ β✝ : Type} [Repr α✝] [Repr β✝] : Repr (PMap α✝ β✝)

Equations

• instReprPMap = { reprPrec := instReprPMap.repr }

@[implicit_reducible]

instance instInhabitedPMap {a✝ a✝¹ : Type} : Inhabited (PMap a✝ a✝¹)

Equations

• instInhabitedPMap = { default := instInhabitedPMap.default }

def PMap.get {α β : Type} [BEq α] (map : PMap α β) (k : α) : Option β

Let k ∈ α and v ∈ β, then PMap.get(k) returns some v (v wrapped inside an option object), when k is assigned to some v. Return none, else.

Equations

• PMap.empty.get k = none
• p(a ↦ a_1; a_2).get k = if (k == a) = true then some a_1 else a_2.get k

def PMap.getKeysAux {α β : Type} [BEq α] [LawfulBEq α] (map : PMap α β) (list : List α) : List α

Accumulate the keys of a PMap onto list, used by getKeys.

Equations

• PMap.empty.getKeysAux list = list
• p(a ↦ a_1; a_2).getKeysAux list = a_2.getKeysAux (a :: list)

def PMap.getKeys {α β : Type} [BEq α] [LawfulBEq α] (map : PMap α β) : List α

Get all keys of a PMap as a list.

Equations

• map.getKeys = map.getKeysAux []

def PMap.toStringAux {α β : Type} [ToString α] [ToString β] (p : PMap α β) : String

Render the bindings of a PMap as a ; -separated string, used by toString.

Equations

• PMap.empty.toStringAux = toString "()"
• p(a ↦ a_1; a_2).toStringAux = toString a ++ toString " ↦ " ++ toString a_1 ++ toString "; " ++ a_2.toStringAux ++ ""

def PMap.toString {α β : Type} [ToString α] [ToString β] (p : PMap α β) : String

Render a PMap as a parenthesised string of its bindings.

Equations

• p.toString = "p(" ++ p.toStringAux ++ ")"

@[implicit_reducible]

instance instReprPMapOfToString {α β : Type} [ToString α] [ToString β] : Repr (PMap α β)

Equations

• instReprPMapOfToString = { reprPrec := fun (p : PMap α β) (x : Nat) => Std.Format.text p.toString }

def «termP(_↦_;_)» : Lean.ParserDescr

Notation p(k ↦ v; m) for inserting the binding k ↦ v into the partial map m.

Equations

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

@[simp]

theorem t_update_eq (α β : Type) [BEq α] [LawfulBEq α] (t : TMap α β) (k : α) (v : β) : (k ↦ v; t).get k = v

This theorem states, when a given map [t] which contains the key [k] with the value [v] as last entry, the function TMap.get returns the corresponding value [v].

@[simp]

theorem t_update_neq (α β : Type) [BEq α] [LawfulBEq α] (t : TMap α β) (k k' : α) (v : β) : k ≠ k' → (k ↦ v; t).get k' = t.get k'

If a total map [t] is updated with some k ∈ α and v ∈ β (k ↦ v; t), and we search for some key [k'] with k ≠ k', we get the same result as when we would just search [t] for [k'].

@[simp]

theorem p_update_eq (α β : Type) [BEq α] [LawfulBEq α] (p : PMap α β) (k : α) (v : β) : p(k ↦ v; p).get k = some v

This theorem states, when a given map [p] which contains the key [k] with the value [v] as last entry, the function PMap.get returns the corresponding value [v].

@[simp]

theorem p_update_neq (α β : Type) [BEq α] [LawfulBEq α] (p : PMap α β) (k k' : α) (v : β) : k ≠ k' → p(k ↦ v; p).get k' = p.get k'

If a partial map [p] is updated with some k ∈ α and v ∈ β (k ↦ v; p), and we search for some key [k'] with k ≠ k', we get the same result as when we would just search [t] for [k'].