data.rbmap.basic - mathlib docs

source

def rbmap_lt {α : Type u} {β : Type v} (lt : α → α → Prop) (a b : α × β) :

Prop

Equations

rbmap_lt lt a b = lt a.fst b.fst

source

def rbmap (α : Type u) (β : Type v) (lt : α → α → Prop . "default_lt") :

Type (max u v)

Equations

rbmap α β lt = rbtree (α × β) (rbmap_lt lt)

source

def mk_rbmap (α : Type u) (β : Type v) (lt : α → α → Prop . "default_lt") :

rbmap α β lt

Equations

mk_rbmap α β lt = mk_rbtree (α × β) (rbmap_lt lt)

source

def rbmap.empty {α : Type u} {β : Type v} {lt : α → α → Prop} (m : rbmap α β lt) :

bool

Equations

m.empty = rbtree.empty m

source

def rbmap.to_list {α : Type u} {β : Type v} {lt : α → α → Prop} (m : rbmap α β lt) :

list (α × β)

Equations

m.to_list = rbtree.to_list m

source

def rbmap.min {α : Type u} {β : Type v} {lt : α → α → Prop} (m : rbmap α β lt) :

option (α × β)

Equations

m.min = rbtree.min m

source

def rbmap.max {α : Type u} {β : Type v} {lt : α → α → Prop} (m : rbmap α β lt) :

option (α × β)

Equations

m.max = rbtree.max m

source

def rbmap.fold {α : Type u} {β : Type v} {δ : Type w} {lt : α → α → Prop} (f : α → β → δ → δ) (m : rbmap α β lt) (d : δ) :

δ

Equations

rbmap.fold f m d = rbtree.fold (λ (e : α × β), f e.fst e.snd) m d

source

def rbmap.rev_fold {α : Type u} {β : Type v} {δ : Type w} {lt : α → α → Prop} (f : α → β → δ → δ) (m : rbmap α β lt) (d : δ) :

δ

Equations

rbmap.rev_fold f m d = rbtree.rev_fold (λ (e : α × β), f e.fst e.snd) m d

source

@[protected]

def rbmap.mem {α : Type u} {β : Type v} {lt : α → α → Prop} (k : α) (m : rbmap α β lt) :

Prop

Equations

rbmap.mem k m = rbmap.mem._match_1 k m m.val
rbmap.mem._match_1 k m (_x.black_node e _x_1) = rbtree.mem (k, e.snd) m
rbmap.mem._match_1 k m (_x.red_node e _x_1) = rbtree.mem (k, e.snd) m
rbmap.mem._match_1 k m rbnode.leaf = false

source

@[protected, instance]

def rbmap.has_mem {α : Type u} {β : Type v} {lt : α → α → Prop} :

has_mem α (rbmap α β lt)

Equations

rbmap.has_mem = {mem := rbmap.mem lt}

source

@[protected, instance]

def rbmap.has_repr {α : Type u} {β : Type v} {lt : α → α → Prop} [has_repr α] [has_repr β] :

has_repr (rbmap α β lt)

Equations

rbmap.has_repr = {repr := λ (t : rbmap α β lt), "rbmap_of " ++ repr t.to_list}

source

def rbmap.rbmap_lt_dec {α : Type u} {β : Type v} {lt : α → α → Prop} [h : decidable_rel lt] :

decidable_rel (rbmap_lt lt)

Equations

rbmap.rbmap_lt_dec = λ (a b : α × β), h a.fst b.fst

source

def rbmap.insert {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] (m : rbmap α β lt) (k : α) (v : β) :

rbmap α β lt

Equations

m.insert k v = rbtree.insert m (k, v)

source

def rbmap.find_entry {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] (m : rbmap α β lt) (k : α) :

option (α × β)

Equations

m.find_entry k = rbmap.find_entry._match_1 m k m.val
rbmap.find_entry._match_1 m k (_x.black_node e _x_1) = rbtree.find m (k, e.snd)
rbmap.find_entry._match_1 m k (_x.red_node e _x_1) = rbtree.find m (k, e.snd)
rbmap.find_entry._match_1 m k rbnode.leaf = none

source

def rbmap.to_value {α : Type u} {β : Type v} :

option (α × β) → option β

Equations

rbmap.to_value (some e) = some e.snd
rbmap.to_value none = none

source

def rbmap.find {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] (m : rbmap α β lt) (k : α) :

option β

Equations

m.find k = rbmap.to_value (m.find_entry k)

source

def rbmap.contains {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] (m : rbmap α β lt) (k : α) :

bool

Equations

m.contains k = (m.find_entry k).is_some

source

def rbmap.from_list {α : Type u} {β : Type v} (l : list (α × β)) (lt : α → α → Prop . "default_lt") [decidable_rel lt] :

rbmap α β lt

Equations

rbmap.from_list l lt = list.foldl (λ (m : rbmap α β lt) (p : α × β), m.insert p.fst p.snd) (mk_rbmap α β lt) l

source

def rbmap_of {α : Type u} {β : Type v} (l : list (α × β)) (lt : α → α → Prop . "default_lt") [decidable_rel lt] :

rbmap α β lt

Equations

rbmap_of l lt = rbmap.from_list l lt