mathlib3 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.filter {key : Type} (s : native.rb_set key) (P : key bool) :

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

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

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

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.

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 α) :

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

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

Declarations about rb_lmap #

@[protected, instance]
meta def native.rb_lmap.inhabited (key : Type) [has_lt key] [decidable_rel has_lt.lt] (data : Type) :
@[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.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.

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

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

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')]