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

@[instance]

meta def native.rb_set.filter {key : Type} :
native.rb_set key(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} :
native.rb_set key(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} :

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} :
native.rb_set keylist keynative.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 keynative.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} :

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} :
native.rb_set keylist keynative.rb_set key

insert_list s l inserts each element of l into s.

Declarations about rb_map

@[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} :
value → native.rb_map key valuekey → 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] :
native.rb_map key valuekey → 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] :
native.rb_map key valuekey → 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] :
native.rb_map key valuenative.rb_map key valuenative.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] :
(key → val → m bool)native.rb_map key valm (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] :
(val → m val')native.rb_map key valm (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] :
value → native.rb_map key valuenative.rb_map key value

scale b m multiplies every value in m by b.

Declarations about rb_lmap

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

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

meta def native.rb_lmap.values {key data : Type} :
native.rb_lmap key datalist data

Returns the list of values of an rb_lmap.

Declarations about name_set

@[instance]

meta def name_set.filter  :
(namebool)name_setname_set

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

meta def name_set.mfilter {m : Type → Type} [monad m] :
(namem bool)name_setm 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] :
(namem name)name_setm name_set

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

meta def name_set.union  :

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

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

@[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.