mathlib documentation

core.init.meta.rb_map

source
meta constant native.rb_map (a : Type u₁) (a_1 : Type u₂) :
Type (max u₁ u₂)

source
meta constant native.rb_map.mk_core {key : Type} (data : Type) (a : key → key → ordering) :
native.rb_map key data

source
meta constant native.rb_map.size {key data : Type} (a : native.rb_map key data) :
ℕ

source
meta constant native.rb_map.empty {key data : Type} (a : native.rb_map key data) :
bool

source
meta constant native.rb_map.insert {key data : Type} (a : native.rb_map key data) (a_1 : key) (a_2 : data) :
native.rb_map key data

source
meta constant native.rb_map.erase {key data : Type} (a : native.rb_map key data) (a_1 : key) :
native.rb_map key data

source
meta constant native.rb_map.contains {key data : Type} (a : native.rb_map key data) (a_1 : key) :
bool

source
meta constant native.rb_map.find {key data : Type} (a : native.rb_map key data) (a_1 : key) :
option data

source
meta constant native.rb_map.min {key data : Type} (a : native.rb_map key data) :
option data

source
meta constant native.rb_map.max {key data : Type} (a : native.rb_map key data) :
option data

source
meta constant native.rb_map.fold {key data α : Type} (a : native.rb_map key data) (a_1 : α) (a_2 : 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] (a : 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] (a : 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
@[instance]
meta def native.has_to_format {key data : Type} [has_to_format key] [has_to_format data] :
has_to_format (native.rb_map key data)

source
@[instance]
meta def native.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
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
@[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 (a : name_set) (a_1 : name) :
name_set

source
meta constant name_set.erase (a : name_set) (a_1 : name) :
name_set

source
meta constant name_set.contains (a : name_set) (a_1 : name) :
bool

source
meta constant name_set.size (a : name_set) :
ℕ

source
meta constant name_set.empty (a : name_set) :
bool

source
meta constant name_set.fold {α : Type} (a : name_set) (a_1 : α) (a_2 : name → α → α) :
α

source
meta def name_set.to_list (s : name_set) :
list name

source
@[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 α