mathlib documentation

core / init.meta.rb_map

meta constant native.rb_map  :
Type u₁Type u₂Type (max u₁ u₂)
meta constant native.rb_map.mk_core {key : Type} (data : Type) :
(key → key → ordering)native.rb_map key data
meta constant native.rb_map.size {key data : Type} :
native.rb_map key data
meta constant native.rb_map.empty {key data : Type} :
native.rb_map key databool
meta constant native.rb_map.insert {key data : Type} :
native.rb_map key datakey → data → native.rb_map key data
meta constant native.rb_map.erase {key data : Type} :
native.rb_map key datakey → native.rb_map key data
meta constant native.rb_map.contains {key data : Type} :
native.rb_map key datakey → bool
meta constant native.rb_map.find {key data : Type} :
native.rb_map key datakey → option data
meta constant native.rb_map.min {key data : Type} :
native.rb_map key dataoption data
meta constant native.rb_map.max {key data : Type} :
native.rb_map key dataoption data
meta constant native.rb_map.fold {key data α : Type} :
native.rb_map key dataα → (key → data → α → α) → α
meta def native.rb_map.mk (key : Type) [has_lt key] [decidable_rel has_lt.lt] (data : Type) :
native.rb_map key data
meta def native.rb_map.keys {key data : Type} (m : native.rb_map key data) :
list key
meta def native.rb_map.values {key data : Type} (m : native.rb_map key data) :
list data
meta def native.rb_map.to_list {key data : Type} (m : native.rb_map key data) :
list (key × data)
meta def native.rb_map.mfold {key data α : Type} {m : Type → Type} [monad m] (mp : native.rb_map key data) (a : α) (fn : key → data → α → m α) :
m α
meta def native.rb_map.of_list {key data : Type} [has_lt key] [decidable_rel has_lt.lt] :
list (key × data)native.rb_map key data
meta def native.rb_map.set_of_list {key : Type} [has_lt key] [decidable_rel has_lt.lt] :
list keynative.rb_map key unit
meta def native.rb_map.map {key data data' : Type} [has_lt key] [decidable_rel has_lt.lt] (f : data → data') (m : native.rb_map key data) :
native.rb_map key data'
meta def native.rb_map.for {key data data' : Type} [has_lt key] [decidable_rel has_lt.lt] (m : native.rb_map key data) (f : data → data') :
native.rb_map key data'
meta def native.rb_map.filter {key data : Type} [has_lt key] [decidable_rel has_lt.lt] (m : native.rb_map key data) (f : data → Prop) [decidable_pred f] :
native.rb_map key data
meta def native.mk_rb_map {key data : Type} [has_lt key] [decidable_rel has_lt.lt] :
native.rb_map key data
meta def native.nat_map (data : Type) :
Type
meta def native.nat_map.mk (data : Type) :
meta def native.mk_nat_map {data : Type} :
@[instance]
meta def native.rb_map.has_to_format {key data : Type} [has_to_format key] [has_to_format data] :
@[instance]
meta def native.rb_map.has_to_string {key data : Type} [has_to_string key] [has_to_string data] :
meta def native.rb_lmap (key data : Type) :
Type

a variant of rb_maps that stores a list of elements for each key. find returns the list of elements in the opposite order that they were inserted.

meta def native.rb_lmap.mk (key : Type) [has_lt key] [decidable_rel has_lt.lt] (data : Type) :
meta def native.rb_lmap.insert {key data : Type} (rbl : native.rb_lmap key data) (k : key) (d : data) :
meta def native.rb_lmap.erase {key data : Type} (rbl : native.rb_lmap key data) (k : key) :
meta def native.rb_lmap.contains {key data : Type} (rbl : native.rb_lmap key data) (k : key) :
meta def native.rb_lmap.find {key data : Type} (rbl : native.rb_lmap key data) (k : key) :
list data
meta def native.rb_set (key : Type u_1) :
Type u_1
meta def native.mk_rb_set {key : Type} [has_lt key] [decidable_rel has_lt.lt] :
meta def native.rb_set.insert {key : Type} (s : native.rb_set key) (k : key) :
meta def native.rb_set.erase {key : Type} (s : native.rb_set key) (k : key) :
meta def native.rb_set.contains {key : Type} (s : native.rb_set key) (k : key) :
meta def native.rb_set.size {key : Type} (s : native.rb_set key) :
meta def native.rb_set.empty {key : Type} (s : native.rb_set key) :
meta def native.rb_set.fold {key α : Type} (s : native.rb_set key) (a : α) (fn : key → α → α) :
α
meta def native.rb_set.mfold {key α : Type} {m : Type → Type} [monad m] (s : native.rb_set key) (a : α) (fn : key → α → m α) :
m α
meta def native.rb_set.to_list {key : Type} (s : native.rb_set key) :
list key
@[instance]
meta def name_map (data : Type) :
Type
meta def name_map.mk (data : Type) :
meta def mk_name_map {data : Type} :
meta constant name_set  :
Type

An rb_map of names.

meta constant mk_name_set  :
meta constant name_set.insert  :
meta constant name_set.erase  :
meta constant name_set.contains  :
meta constant name_set.size  :
meta constant name_set.empty  :
meta constant name_set.fold {α : Type} :
name_setα → (nameα → α) → α
meta def name_set.union (l r : name_set) :
meta def name_set.mfold {α : Type} {m : Type → Type} [monad m] (ns : name_set) (a : α) (fn : nameα → m α) :
m α