mathlib docs: core.init.meta.rb

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} :

native.rb_map key data → list key

source

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

native.rb_map key data → list data

source

meta def native.rb_map.to_list {key data : Type} :

native.rb_map key data → list (key × data)

source

meta def native.rb_map.mfold {key data α : Type} {m : Type → Type} [monad m] :

native.rb_map key data → α → (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] :

(data → data') → 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] :

native.rb_map key data → (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 :

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 :

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.

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} :

native.rb_lmap key data → key → data → native.rb_lmap key data

source

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

native.rb_lmap key data → key → native.rb_lmap key data

source

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

native.rb_lmap key data → key → bool

source

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

native.rb_lmap key data → key → list data

source

meta def native.rb_set :

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} :

native.rb_set key → key → native.rb_set key

source

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

native.rb_set key → key → native.rb_set key

source

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

native.rb_set key → key → bool

source

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

native.rb_set key → ℕ

source

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

native.rb_set key → bool

source

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

native.rb_set key → α → (key → α → α) → α

source

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

native.rb_set key → α → (key → α → m α) → m α

source

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

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 :

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.to_list :

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 :

list name → name_set

source

meta def name_set.mfold {α : Type} {m : Type → Type} [monad m] :

name_set → α → (name → α → m α) → m α

mathlib documentation

core.init.meta.rb_map

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​meta.​rb_map

General documentation

Additional documentation

Library

core.init.meta.rb_map