mathlib documentation

core.init.data.rbmap.basic

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

Equations
def rbmap (α : Type u) :
Type v(α → α → Prop . "default_lt")Type (max u v)

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

Equations
def rbmap.empty {α : Type u} {β : Type v} {lt : α → α → Prop} :
rbmap α β ltbool

Equations
def rbmap.to_list {α : Type u} {β : Type v} {lt : α → α → Prop} :
rbmap α β ltlist × β)

Equations
def rbmap.min {α : Type u} {β : Type v} {lt : α → α → Prop} :
rbmap α β ltoption × β)

Equations
def rbmap.max {α : Type u} {β : Type v} {lt : α → α → Prop} :
rbmap α β ltoption × β)

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

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

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

Equations
@[instance]
def rbmap.has_mem {α : Type u} {β : Type v} {lt : α → α → Prop} :
has_mem α (rbmap α β lt)

Equations
@[instance]
def rbmap.has_repr {α : Type u} {β : Type v} {lt : α → α → Prop} [has_repr α] [has_repr β] :
has_repr (rbmap α β lt)

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

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

Equations
def rbmap.find_entry {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] :
rbmap α β ltα → option × β)

Equations
def rbmap.to_value {α : Type u} {β : Type v} :
option × β)option β

Equations
def rbmap.find {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] :
rbmap α β ltα → option β

Equations
def rbmap.contains {α : Type u} {β : Type v} {lt : α → α → Prop} [decidable_rel lt] :
rbmap α β ltα → bool

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

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

Equations