mathlib documentation

core / init.meta.rb_map

source
meta constant native.rb_map  :
Type u₁ → Type u₂ → Type (max u₁ u₂)
source
meta constant native.rb_map.mk_core {key : Type} (data : Type) :
(key → key → ordering) → native.rb_map key data
source
meta constant native.rb_map.size {key data : Type} :
native.rb_map key data → ℕ
source
meta constant native.rb_map.empty {key data : Type} :
native.rb_map key data → bool
source
meta constant native.rb_map.insert {key data : Type} :
native.rb_map key data → key → data → native.rb_map key data
source
meta constant native.rb_map.erase {key data : Type} :
native.rb_map key data → key → native.rb_map key data
source
meta constant native.rb_map.contains {key data : Type} :
native.rb_map key data → key → bool
source
meta constant native.rb_map.find {key data : Type} :
native.rb_map key data → key → option data
source
meta constant native.rb_map.min {key data : Type} :
native.rb_map key data → option data
source
meta constant native.rb_map.max {key data : Type} :
native.rb_map key data → option data
source
meta constant native.rb_map.fold {key data α : Type} :
native.rb_map key data → α → (key → data → α → α) → α
source
meta def native.rb_map.mk (key : Type) [has_lt key] [decidable_rel has_lt.lt] (data : Type) :
native.rb_map key data
source
meta def native.rb_map.keys {key data : Type} (m : native.rb_map key data) :
list key
source
meta def native.rb_map.values {key data : Type} (m : native.rb_map key data) :
list data
source
meta def native.rb_map.to_list {key data : Type} (m : native.rb_map key data) :
list (key × data)
source
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 α
source
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
source
meta def native.rb_map.set_of_list {key : Type} [has_lt key] [decidable_rel has_lt.lt] :
list key → native.rb_map key unit
source
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'
source
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'
source
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
source
meta def native.mk_rb_map {key data : Type} [has_lt key] [decidable_rel has_lt.lt] :
native.rb_map key data
source
meta def native.nat_map (data : Type) :
Type
source
meta def native.nat_map.mk (data : Type) :
native.nat_map data
source
meta def native.mk_nat_map {data : Type} :
native.nat_map data
source
@[protected, instance]
meta def native.rb_map.has_to_format {key data : Type} [has_to_format key] [has_to_format data] :
has_to_format (native.rb_map key data)
source
@[protected, instance]
meta def native.rb_map.has_to_string {key data : Type} [has_to_string key] [has_to_string data] :
has_to_string (native.rb_map key data)
source
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.

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

An rb_map of names.

source
meta constant mk_name_set  :
name_set
source
meta constant name_set.insert  :
name_set → name → name_set
source
meta constant name_set.erase  :
name_set → name → name_set
source
meta constant name_set.contains  :
name_set → name → bool
source
meta constant name_set.size  :
name_set → ℕ
source
meta constant name_set.empty  :
name_set → bool
source
meta constant name_set.fold {α : Type} :
name_set → α → (name → α → α) → α
source
meta def name_set.union (l r : name_set) :
name_set
source
meta def name_set.to_list (s : name_set) :
list name
source
@[protected, instance]
meta def name_set.has_to_format  :
has_to_format name_set
source
meta def name_set.of_list (l : list name) :
name_set
source
meta def name_set.mfold {α : Type} {m : Type → Type} [monad m] (ns : name_set) (a : α) (fn : name → α → m α) :
m α