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} :
native.rb_map key datalist key

meta def native.rb_map.values {key data : Type} :
native.rb_map key datalist data

meta def native.rb_map.to_list {key data : Type} :
native.rb_map key datalist (key × data)

meta def native.rb_map.mfold {key data α : Type} {m : Type → Type} [monad m] :
native.rb_map key dataα → (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] :
(data → data')native.rb_map key datanative.rb_map key data'

meta def native.rb_map.for {key data data' : Type} [has_lt key] [decidable_rel has_lt.lt] :
native.rb_map key data(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  :
Type → Type

meta def native.nat_map.mk (data : Type) :

meta def native.mk_nat_map {data : Type} :

@[instance]
meta def native.has_to_format {key data : Type} [has_to_format key] [has_to_format data] :

@[instance]
meta def native.has_to_string {key data : Type} [has_to_string key] [has_to_string data] :

meta def native.rb_lmap  :
Type → 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} :
native.rb_lmap key datakey → data → native.rb_lmap key data

meta def native.rb_lmap.erase {key data : Type} :
native.rb_lmap key datakey → native.rb_lmap key data

meta def native.rb_lmap.contains {key data : Type} :
native.rb_lmap key datakey → bool

meta def native.rb_lmap.find {key data : Type} :
native.rb_lmap key datakey → list data

meta def native.rb_set  :
Type u_1Type 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} :
native.rb_set keykey → native.rb_set key

meta def native.rb_set.erase {key : Type} :
native.rb_set keykey → native.rb_set key

meta def native.rb_set.contains {key : Type} :
native.rb_set keykey → bool

meta def native.rb_set.size {key : Type} :

meta def native.rb_set.empty {key : Type} :

meta def native.rb_set.fold {key α : Type} :
native.rb_set keyα → (key → α → α) → α

meta def native.rb_set.mfold {key α : Type} {m : Type → Type} [monad m] :
native.rb_set keyα → (key → α → m α)m α

meta def native.rb_set.to_list {key : Type} :
native.rb_set keylist key

@[instance]

meta def name_map  :
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.mfold {α : Type} {m : Type → Type} [monad m] :
name_setα → (nameα → m α)m α