mathlib3 documentation

core / init.meta.rb_map

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} :
meta constant native.rb_map.empty {key data : Type} :
meta constant native.rb_map.insert {key data : Type} :
native.rb_map key data key data native.rb_map key data
meta constant native.rb_map.erase {key data : Type} :
native.rb_map key data key native.rb_map key data
meta constant native.rb_map.contains {key data : Type} :
native.rb_map key data key bool
meta constant native.rb_map.find {key data : Type} :
native.rb_map key data key option data
meta constant native.rb_map.min {key data : Type} :
native.rb_map key data option data
meta constant native.rb_map.max {key data : Type} :
native.rb_map key data option 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.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
@[reducible]
meta def native.nat_map (data : Type) :
meta def native.nat_map.mk (data : Type) :
meta def native.mk_nat_map {data : Type} :
@[protected, instance]
meta def native.rb_map.has_to_format {key data : Type} [has_to_format key] [has_to_format data] :
@[protected, 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) :

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.

Instances for native.rb_lmap
@[protected]
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.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
@[protected, instance]
@[reducible]
meta def name_map (data : Type) :
meta def name_map.mk (data : Type) :
meta def mk_name_map {data : Type} :
meta constant name_set  :

An rb_map of names.

Instances for name_set
meta constant mk_name_set  :
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) :
@[protected, instance]
meta def name_set.mfold {α : Type} {m : Type Type} [monad m] (ns : name_set) (a : α) (fn : name α m α) :
m α