mathlib documentation

meta.rb_map

rb_map #

This file defines additional operations on native rb_maps and rb_sets. These structures are defined in core in init.meta.rb_map. They are meta objects, and are generally the most efficient dictionary structures to use for pure metaprogramming right now.

Declarations about `rb_set` #

@[protected, instance]

meta def native.rb_set.inhabited {key : Type} [has_lt key] [decidable_rel has_lt.lt] :

inhabited (native.rb_set key)

meta def native.rb_set.filter {key : Type} (s : native.rb_set key) (P : key → bool) :

native.rb_set key

filter s P returns the subset of elements of s satisfying P.

meta def native.rb_set.mfilter {m : Type → Type} [monad m] {key : Type} (s : native.rb_set key) (P : key → m bool) :

m (native.rb_set key)

mfilter s P returns the subset of elements of s satisfying P, where the check P is monadic.

meta def native.rb_set.union {key : Type} (s t : native.rb_set key) :

native.rb_set key

union s t returns an rb_set containing every element that appears in either s or t.

meta def native.rb_set.of_list_core {key : Type} (base : native.rb_set key) :

list key → native.rb_map key unit

of_list_core empty l turns a list of keys into an rb_set. It takes a user_provided rb_set to use for the base case. This can be used to pre-seed the set with additional elements, and/or to use a custom comparison operator.

meta def native.rb_set.of_list {key : Type} [has_lt key] [decidable_rel has_lt.lt] :

list key → native.rb_set key

of_list l transforms a list l : list key into an rb_set, inferring an order on the type key.

meta def native.rb_set.sdiff {α : Type} (s1 s2 : native.rb_set α) :

native.rb_set α

sdiff s1 s2 returns the set of elements that are in s1 but not in s2. It does so by folding over s2. If s1 is significantly smaller than s2, it may be worth it to reverse the fold.

meta def native.rb_set.insert_list {key : Type} (s : native.rb_set key) (l : list key) :

native.rb_set key

insert_list s l inserts each element of l into s.

Declarations about `rb_map` #

@[protected, instance]

meta def native.rb_map.inhabited {key data : Type} [has_lt key] [decidable_rel has_lt.lt] :

inhabited (native.rb_map key data)

meta def native.rb_map.find_def {key value : Type} (default : value) (m : native.rb_map key value) (k : key) :

value

find_def default m k returns the value corresponding to k in m, if it exists. Otherwise it returns default.

meta def native.rb_map.ifind {key value : Type} [inhabited value] (m : native.rb_map key value) (k : key) :

value

ifind m key returns the value corresponding to key in m, if it exists. Otherwise it returns the default value of value.

meta def native.rb_map.zfind {key value : Type} [has_zero value] (m : native.rb_map key value) (k : key) :

value

zfind m key returns the value corresponding to key in m, if it exists. Otherwise it returns 0.

meta def native.rb_map.add {key value : Type} [has_add value] [has_zero value] [decidable_eq value] (m1 m2 : native.rb_map key value) :

native.rb_map key value

Returns the pointwise sum of m1 and m2, treating nonexistent values as 0.

meta def native.rb_map.mfilter {m : Type → Type u_1} [monad m] {key val : Type} [has_lt key] [decidable_rel has_lt.lt] (P : key → val → m bool) (s : native.rb_map key val) :

m (native.rb_map key val)

mfilter P s filters s by the monadic predicate P on keys and values.

meta def native.rb_map.mmap {m : Type → Type u_1} [monad m] {key val val' : Type} [has_lt key] [decidable_rel has_lt.lt] (f : val → m val') (s : native.rb_map key val) :

m (native.rb_map key val')

mmap f s maps the monadic function f over values in s.

meta def native.rb_map.scale {key value : Type} [has_lt key] [decidable_rel has_lt.lt] [has_mul value] (b : value) (m : native.rb_map key value) :

native.rb_map key value

scale b m multiplies every value in m by b.

@[protected, instance]

meta def native.rb_map.has_to_tactic_format {key data : Type} [has_to_tactic_format key] [has_to_tactic_format data] :

has_to_tactic_format (native.rb_map key data)

Declarations about `rb_lmap` #

@[protected, instance]

meta def native.rb_lmap.inhabited (key : Type) [has_lt key] [decidable_rel has_lt.lt] (data : Type) :

inhabited (native.rb_lmap key data)

@[protected]

meta def native.rb_lmap.of_list {key data : Type} [has_lt key] [decidable_rel has_lt.lt] :

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

Construct a rb_lmap from a list of key-data pairs

@[protected]

meta def native.rb_lmap.values {key data : Type} (m : native.rb_lmap key data) :

list data

Returns the list of values of an rb_lmap.

Declarations about `name_set` #

@[protected, instance]

meta def name_set.inhabited :

inhabited name_set

meta def name_set.filter (P : name → bool) (s : name_set) :

filter P s returns the subset of elements of s satisfying P.

meta def name_set.mfilter {m : Type → Type} [monad m] (P : name → m bool) (s : name_set) :

mfilter P s returns the subset of elements of s satisfying P, where the check P is monadic.

meta def name_set.mmap {m : Type → Type} [monad m] (f : name → m name) (s : name_set) :

mmap f s maps the monadic function f over values in s.

meta def name_set.insert_list (s : name_set) (l : list name) :

insert_list s l inserts every element of l into s.

meta def name_set.local_list_to_name_set (lcs : list expr) :

local_list_to_name_set lcs is the set of unique names of the local constants lcs. If any of the lcs are not local constants, the returned set will contain bogus names.

Declarations about `name_map` #

@[protected, instance]

meta def name_map.inhabited {data : Type} :

inhabited (name_map data)

Declarations about `expr_set` #

meta def expr_set.local_set_to_name_set (lcs : expr_set) :

local_set_to_name_set lcs is the set of unique names of the local constants lcs. If any of the lcs are not local constants, the returned set will contain bogus names.

meta def list.to_rb_map {α : Type} :

list α → native.rb_map ℕ α

to_rb_map as is the map that associates each index i of as with the corresponding element of as.

to_rb_map ['a', 'b', 'c'] = rb_map.of_list [(0, 'a'), (1, 'b'), (2, 'c')]