mathlib3 documentation

data.rbmap.basic

def rbmap_lt {α : Type u} {β : Type v} (lt : α α Prop) (a b : α × β) :
Prop
Equations
def rbmap (α : Type u) (β : Type v) (lt : α α Prop . "default_lt") :
Type (max u v)
Equations
Instances for rbmap
def mk_rbmap (α : Type u) (β : Type v) (lt : α α Prop . "default_lt") :
rbmap α β lt
Equations
def rbmap.empty {α : Type u} {β : Type v} {lt : α α Prop} (m : rbmap α β lt) :
Equations
def rbmap.to_list {α : Type u} {β : Type v} {lt : α α Prop} (m : rbmap α β lt) :
list × β)
Equations
def rbmap.min {α : Type u} {β : Type v} {lt : α α Prop} (m : rbmap α β lt) :
option × β)
Equations
def rbmap.max {α : Type u} {β : Type v} {lt : α α Prop} (m : rbmap α β lt) :
option × β)
Equations
def rbmap.fold {α : Type u} {β : Type v} {δ : Type w} {lt : α α Prop} (f : α β δ δ) (m : rbmap α β lt) (d : δ) :
δ
Equations
def rbmap.rev_fold {α : Type u} {β : Type v} {δ : Type w} {lt : α α Prop} (f : α β δ δ) (m : rbmap α β lt) (d : δ) :
δ
Equations
@[protected]
def rbmap.mem {α : Type u} {β : Type v} {lt : α α Prop} (k : α) (m : rbmap α β lt) :
Prop
Equations
@[protected, instance]
def rbmap.has_mem {α : Type u} {β : Type v} {lt : α α Prop} :
has_mem α (rbmap α β lt)
Equations
@[protected, 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] (m : rbmap α β lt) (k : α) (v : β) :
rbmap α β lt
Equations
def rbmap.find_entry {α : Type u} {β : Type v} {lt : α α Prop} [decidable_rel lt] (m : rbmap α β lt) (k : α) :
option × β)
Equations
def rbmap.find {α : Type u} {β : Type v} {lt : α α Prop} [decidable_rel lt] (m : rbmap α β lt) (k : α) :
Equations
def rbmap.contains {α : Type u} {β : Type v} {lt : α α Prop} [decidable_rel lt] (m : rbmap α β lt) (k : α) :
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