meta.expr - mathlib3 docs

If nm is a simple name (having only one string component) starting with _, then deinternalize_field nm removes the underscore. Otherwise, it does nothing.

source

meta def name.get_nth_prefix :

name → ℕ → name

get_nth_prefix nm n removes the last n components from nm

source

meta def name.pop_nth_prefix (nm : name) (n : ℕ) :

name

Pops the top n prefixes from the given name.

source

meta def name.pop_prefix (n : name) :

name

Pop the prefix of a name

source

def name.from_components :

list string → name

Build a name from components. For example from_components ["foo","bar"] becomes `foo.bar

Equations

name.from_components = from_components_aux name.anonymous

source

meta def name.sanitize_name :

name → name

names can contain numeral pieces, which are not legal names when typed/passed directly to the parser. We turn an arbitrary name into a legal identifier name by turning the numbers to strings.

source

def name.append_suffix :

name → string → name

Append a string to the last component of a name.

Equations

(name.mk_numeral ᾰ ᾰ_1).append_suffix _x = name.mk_numeral ᾰ ᾰ_1
(name.mk_string s n).append_suffix s' = name.mk_string (s ++ s') n
name.anonymous.append_suffix _x = name.anonymous

source

def name.update_last (f : string → string) :

name → name

Update the last component of a name.

Equations

name.update_last f (name.mk_numeral ᾰ ᾰ_1) = name.mk_numeral ᾰ ᾰ_1
name.update_last f (name.mk_string s n) = name.mk_string (f s) n
name.update_last f name.anonymous = name.anonymous

source

def name.append_to_last (nm : name) (s : string) (is_prefix : bool) :

name

append_to_last nm s is_prefix adds s to the last component of nm, either as prefix or as suffix (specified by is_prefix), separated by _. Used by simps_add_projections.

Equations

nm.append_to_last s is_prefix = name.update_last (λ (s' : string), ite ↥is_prefix (s ++ "_" ++ s') (s' ++ "_" ++ s)) nm

source

meta def name.head :

name → string

The first component of a name, turning a number to a string

source

meta def name.is_private (n : name) :

bool

Tests whether the first component of a name is "_private"

source

meta def name.length :

name → ℕ

Returns the number of characters used to print all the string components of a name, including periods between name segments. Ignores numerical parts of a name.

source

def name.has_prefix (P : name → bool) :

name → bool

Checks whether nm has a prefix (including itself) such that P is true

Equations

name.has_prefix P (name.mk_numeral s nm) = decidable.to_bool (↥(P (name.mk_numeral s nm)) ∨ ↥(name.has_prefix P nm))
name.has_prefix P (name.mk_string s nm) = decidable.to_bool (↥(P (name.mk_string s nm)) ∨ ↥(name.has_prefix P nm))
name.has_prefix P name.anonymous = bool.ff

source

meta def name.add_prime :

name → name

Appends ' to the end of a name.

source

def name.last_string :

name → string

last_string n returns the rightmost component of n, ignoring numeral components. For example, last_string `a.b.c.33 will return `c.

Equations

(name.mk_numeral _x n).last_string = n.last_string
(name.mk_string s _x).last_string = s
name.anonymous.last_string = "[anonymous]"

source

meta def name.append_namespace (ns : name) :

name → name

Like ++, except that if the right argument starts with _root_ the namespace will be ignored.

append_namespace `a.b `c.d = `a.b.c.d
append_namespace `a.b `_root_.c.d = `c.d

source

meta def name.from_string (s : string) :

name

Constructs a (non-simple) name from a string.

Example: name.from_string "foo.bar" = `foo.bar

source

def library_note.likely generated binder names :

unit

In surface Lean, we can write anonymous Π binders (i.e. binders where the argument is not named) using the function arrow notation:

inductive test : Type
| intro : unit → test

After elaboration, however, every binder must have a name, so Lean generates one. In the example, the binder in the type of intro is anonymous, so Lean gives it the name ᾰ:

test.intro : ∀ (ᾰ : unit), test

When there are multiple anonymous binders, they are named ᾰ_1, ᾰ_2 etc.

Thus, when we want to know whether the user named a binder, we can check whether the name follows this scheme. Note, however, that this is not reliable. When the user writes (for whatever reason)

inductive test : Type
| intro : ∀ (ᾰ : unit), test

we cannot tell that the binder was, in fact, named.

The function name.is_likely_generated_binder_name checks if a name is of the form ᾰ, ᾰ_1, etc.

source

meta def name.is_likely_generated_binder_simple_name :

string → bool

Check whether a simple name was likely generated by Lean to name an anonymous binder. Such names are either ᾰ or ᾰ_n for some natural n. See note [likely generated binder names].

source

meta def name.is_likely_generated_binder_name (n : name) :

bool

Check whether a name was likely generated by Lean to name an anonymous binder. Such names are either ᾰ or ᾰ_n for some natural n. See note [likely generated binder names].

source

meta def level.nonzero :

level → bool

Tests whether a universe level is non-zero for all assignments of its variables

source

meta def level.fold_mvar {α : Sort u_1} :

level → (name → α → α) → α → α

l.fold_mvar f folds a function f : name → α → α over each n : name appearing in a level.mvar n in l.

source

@[protected]

meta def level.params (u : level) :

name_set

l.params is the set of parameters occuring in l. For example if l = max 1 (max (u+1) (max v w)) then l.params = {u, v, w}.

source

@[protected, instance]

meta def binder.decidable_eq :

decidable_eq binder

source

meta structure binder :

Type

name : name
info : binder_info
type : expr

The type of binders containing a name, the binding info and the binding type

Instances for binder

source

@[protected, instance]

meta def binder.inhabited :

inhabited binder

source

@[protected]

meta def binder.to_string (b : binder) :

string

Turn a binder into a string. Uses expr.to_string for the type.

source

@[protected, instance]

meta def binder.has_to_string :

has_to_string binder

source

@[protected, instance]

meta def binder.has_to_format :

has_to_format binder

source

@[protected, instance]

meta def binder.has_to_tactic_format :

has_to_tactic_format binder

source

meta def nat.mk_numeral (type has_zero has_one has_add : expr) :

ℕ → expr

nat.mk_numeral n embeds n as a numeral expression inside a type with 0, 1, and +. type: an expression representing the target type. This must live in Type 0. has_zero, has_one, has_add: expressions of the type has_zero %%type, etc.

source

meta def int.mk_numeral (type has_zero has_one has_add has_neg : expr) :

ℤ → expr

int.mk_numeral z embeds z as a numeral expression inside a type with 0, 1, +, and -. type: an expression representing the target type. This must live in Type 0. has_zero, has_one, has_add, has_neg: expressions of the type has_zero %%type, etc.

source

meta def nat.to_pexpr :

ℕ → pexpr

nat.to_pexpr n creates a pexpr that will evaluate to n. The pexpr does not hold any typing information: to_expr ``((%%(nat.to_pexpr 5) : ℤ)) will create a native integer numeral (5 : ℤ).

source

meta def int.to_pexpr :

ℤ → pexpr

int.to_pexpr n creates a pexpr that will evaluate to n. The pexpr does not hold any typing information: to_expr ``((%%(int.to_pexpr (-5)) : ℚ)) will create a native ℚ numeral (-5 : ℚ).

source

@[protected]

meta def expr.to_nat :

expr → option ℕ

Turns an expression into a natural number, assuming it is only built up from has_one.one, bit0, bit1, has_zero.zero, nat.zero, and nat.succ.

source

@[protected]

meta def expr.to_int :

expr → option ℤ

Turns an expression into a integer, assuming it is only built up from has_one.one, bit0, bit1, has_zero.zero and a optionally a single has_neg.neg as head.

source

@[protected]

meta def expr.to_list {α : Type u_1} (f : expr → option α) :

expr → option (list α)

Turns an expression into a list, assuming it is only built up from list.nil and list.cons.

source

meta def expr.is_num_eq :

expr → expr → bool

is_num_eq n1 n2 returns true if n1 and n2 are both numerals with the same numeral structure, ignoring differences in type and type class arguments.

source

meta def pexpr.get_frozen_name (e : pexpr) :

name

If e is an annotation of frozen_name to expr.const n, e.get_frozen_name returns n. Otherwise, returns name.anonymous.

source

meta def pexpr.get_app_fn_args :

pexpr → (list pexpr := list.nil) → pexpr × list pexpr

If e : pexpr is a sequence of applications f e₁ e₂ ... eₙ, e.get_app_fn_args returns (f, [e₁, ... eₙ]). See also expr.get_app_fn_args.

source

meta def pexpr.get_app_fn :

pexpr → list pexpr

If e : pexpr is a sequence of applications f e₁ e₂ ... eₙ, e.get_app_fn returns f. See also expr.get_app_fn.

source

meta def pexpr.get_app_args :

pexpr → list pexpr

If e : pexpr is a sequence of applications f e₁ e₂ ... eₙ, e.get_app_args returns [e₁, ... eₙ]. See also expr.get_app_args.

source

meta def expr.clean_ids :

list name

List of names removed by clean. All these names must resolve to functions defeq id.

source

meta def expr.clean (e : expr) :

expr

Clean an expression by removing ids listed in clean_ids.

source

meta def expr.replace_with (e s s' : expr) :

expr

replace_with e s s' replaces ocurrences of s with s' in e.

source

meta def expr.mreplace_aux {m : Type → Type u_1} [monad m] (R : expr → ℕ → m (option expr)) :

expr → ℕ → m expr

Implementation of expr.mreplace.

source

meta def expr.mreplace {m : Type → Type u_1} [monad m] (R : expr → ℕ → m (option expr)) (e : expr) :

m expr

Monadic analogue of expr.replace.

The mreplace R e visits each subexpression s of e, and is called with R s n, where n is the number of binders above e. If R s n fails, the whole replacement fails. If R s n returns some t, s is replaced with t (and mreplace does not visit its subexpressions). If R s n return none, then mreplace continues visiting subexpressions of s.

WARNING: This function performs exponentially worse on large terms than expr.replace, if a subexpression occurs more than once in an expression, expr.replace visits them only once, but this function will visit every occurence of it. Do not use this on large expressions.

source

meta def expr.match_var {elab : bool := bool.tt} :

expr elab → option ℕ

Match a variable.

source

meta def expr.match_sort {elab : bool := bool.tt} :

expr elab → option level

Match a sort.

source

meta def expr.match_const {elab : bool := bool.tt} :

expr elab → option (name × list level)

Match a constant.

source

meta def expr.match_mvar {elab : bool := bool.tt} :

expr elab → option (name × name × expr elab)

Match a metavariable.

source

meta def expr.match_local_const {elab : bool := bool.tt} :

expr elab → option (name × name × binder_info × expr elab)

Match a local constant.

source

meta def expr.match_app {elab : bool := bool.tt} :

expr elab → option (expr elab × expr elab)

Match an application.

source

meta def expr.match_app_coe_fn :

expr → option (expr × expr × expr × expr × expr)

Match an application of coe_fn.

source

meta def expr.match_lam {elab : bool := bool.tt} :

expr elab → option (name × binder_info × expr elab × expr elab)

Match an abstraction.

source

meta def expr.match_pi {elab : bool := bool.tt} :

expr elab → option (name × binder_info × expr elab × expr elab)

Match a Π type.

source

meta def expr.match_elet {elab : bool := bool.tt} :

expr elab → option (name × expr elab × expr elab × expr elab)

Match a let.

source

meta def expr.match_macro {elab : bool := bool.tt} :

expr elab → option (macro_def × list (expr elab))

Match a macro.

source

meta def expr.is_mvar :

expr → bool

Tests whether an expression is a meta-variable.

source

meta def expr.is_sort :

expr → bool

Tests whether an expression is a sort.

source

meta def expr.univ_levels :

expr → list level

Get the universe levels of a const expression

source

meta def expr.replace_mvars (e : expr) :

expr

Replace any metavariables in the expression with underscores, in preparation for printing refine ... statements.

source

meta def expr.to_implicit_local_const :

expr → expr

If e is a local constant, to_implicit_local_const e changes the binder info of e to implicit. See also to_implicit_binder, which also changes lambdas and pis.

source

meta def expr.to_implicit_binder :

expr → expr

If e is a local constant, lamda, or pi expression, to_implicit_binder e changes the binder info of e to implicit. See also to_implicit_local_const, which only changes local constants.

source

meta def expr.list_local_consts (e : expr) :

list expr

Returns a list of all local constants in an expression (without duplicates).

source

meta def expr.list_local_consts' (e : expr) :

expr_set

Returns the set of all local constants in an expression.

source

meta def expr.list_local_const_unique_names (e : expr) :

name_set

Returns the unique names of all local constants in an expression.

source

meta def expr.list_constant (e : expr) :

name_set

Returns a name_set of all constants in an expression.

source

meta def expr.list_constant' (e : expr) :

list name

Returns a list name containing the constant names of an expr in the same order that expr.fold traverses it.

source

meta def expr.list_meta_vars (e : expr) :

list expr

Returns a list of all meta-variables in an expression (without duplicates).

source

meta def expr.list_meta_vars' (e : expr) :

expr_set

Returns the set of all meta-variables in an expression.

source

meta def expr.list_univ_meta_vars (e : expr) :

list name

Returns a list of all universe meta-variables in an expression (without duplicates).

source

meta def expr.contains_expr_or_mvar (t e : expr) :

bool

Test t contains the specified subexpression e, or a metavariable. This represents the notion that e "may occur" in t, possibly after subsequent unification.

source

meta def expr.list_names_with_prefix (pre : name) (e : expr) :

name_set

Returns a name_set of all constants in an expression starting with a certain prefix.

source

meta def expr.contains_constant (e : expr) (p : name → Prop) [decidable_pred p] :

bool

Returns true if e contains a name n where p n is true. Returns true if p name.anonymous is true.

source

meta def expr.contains_sorry (e : expr) :

bool

Returns true if e contains a sorry. See also name.contains_sorry.

source

meta def expr.app_symbol_in (e : expr) (l : list name) :

bool

app_symbol_in e l returns true iff e is an application of a constant whose name is in l.

source

meta def expr.get_simp_args (e : expr) :

tactic (list expr)

get_simp_args e returns the arguments of e that simp can reach via congruence lemmas.

source

meta def expr.simp (t : expr) (cfg : tactic.simp_config := {max_steps := simp.default_max_steps, contextual := bool.ff, lift_eq := bool.tt, canonize_instances := bool.tt, canonize_proofs := bool.ff, use_axioms := bool.tt, zeta := bool.tt, beta := bool.tt, eta := bool.tt, proj := bool.tt, iota := bool.tt, iota_eqn := bool.ff, constructor_eq := bool.tt, single_pass := bool.ff, fail_if_unchanged := bool.tt, memoize := bool.tt, trace_lemmas := bool.ff}) (discharger : tactic unit := tactic.failed) (no_defaults : bool := bool.ff) (attr_names : list name := list.nil) (hs : list tactic.simp_arg_type := list.nil) :

tactic (expr × expr × name_set)

Simplifies the expression t with the specified options. The result is (new_e, pr) with the new expression new_e and a proof pr : e = new_e.

source

meta def expr.dsimp (t : expr) (cfg : tactic.dsimp_config := {md := tactic.transparency.reducible, max_steps := simp.default_max_steps, canonize_instances := bool.tt, single_pass := bool.ff, fail_if_unchanged := bool.tt, eta := bool.tt, zeta := bool.tt, beta := bool.tt, proj := bool.tt, iota := bool.tt, unfold_reducible := bool.ff, memoize := bool.tt}) (no_defaults : bool := bool.ff) (attr_names : list name := list.nil) (hs : list tactic.simp_arg_type := list.nil) :

tactic expr

Definitionally simplifies the expression t with the specified options. The result is the simplified expression.

source

meta def expr.binding_names :

expr → list name

Get the names of the bound variables by a sequence of pis or lambdas.

source

meta def expr.reduce_let :

expr → expr

head-reduce a single let expression

source

meta def expr.reduce_lets :

expr → expr

head-reduce all let expressions

source

meta def expr.instantiate_lambdas :

list expr → expr → expr

Instantiate lambdas in the second argument by expressions from the first.

source

meta def expr.substs :

expr → list expr → expr

Repeatedly apply expr.subst.

source

meta def expr.instantiate_lambdas_or_apps :

list expr → expr → expr

instantiate_lambdas_or_apps es e instantiates lambdas in e by expressions from es. If the length of es is larger than the number of lambdas in e, then the term is applied to the remaining terms. Also reduces head let-expressions in e, including those after instantiating all lambdas.

This is very similar to expr.substs, but this also reduces head let-expressions.

source

def library_note.open expressions :

unit

Some declarations work with open expressions, i.e. an expr that has free variables. Terms will free variables are not well-typed, and one should not use them in tactics like infer_type or unify. You can still do syntactic analysis/manipulation on them. The reason for working with open types is for performance: instantiating variables requires iterating through the expression. In one performance test pi_binders was more than 6x quicker than mk_local_pis (when applied to the type of all imported declarations 100x).

source

meta def expr.pi_codomain :

expr → expr

Get the codomain/target of a pi-type. This definition doesn't instantiate bound variables, and therefore produces a term that is open. See note [open expressions].

source

meta def expr.lambda_body :

expr → expr

Get the body/value of a lambda-expression. This definition doesn't instantiate bound variables, and therefore produces a term that is open. See note [open expressions].

source

meta def expr.pi_binders_aux :

list binder → expr → list binder × expr

Auxiliary defintion for pi_binders. See note [open expressions].

source

meta def expr.pi_binders (e : expr) :

list binder × expr

Get the binders and codomain of a pi-type. This definition doesn't instantiate bound variables, and therefore produces a term that is open. The.tactic get_pi_binders in tactic.core does the same, but also instantiates the free variables. See note [open expressions].

source

meta def expr.get_app_fn_args_aux :

list expr → expr → expr × list expr

Auxiliary defintion for get_app_fn_args.

source

meta def expr.get_app_fn_args :

expr → expr × list expr

A combination of get_app_fn and get_app_args: lists both the function and its arguments of an application

source

meta def expr.drop_pis :

list expr → expr → tactic expr

drop_pis es e instantiates the pis in e with the expressions from es.

source

meta def expr.instantiate_pis :

list expr → expr → expr

instantiate_pis es e instantiates the pis in e with the expressions from es. Does not check whether the result remains type-correct.

source

meta def expr.mk_op_lst (op empty : expr) :

list expr → expr

mk_op_lst op empty [x1, x2, ...] is defined as op x1 (op x2 ...). Returns empty if the list is empty.

source

meta def expr.mk_and_lst :

list expr → expr

mk_and_lst [x1, x2, ...] is defined as x1 ∧ (x2 ∧ ...), or true if the list is empty.

source

meta def expr.mk_or_lst :

list expr → expr

mk_or_lst [x1, x2, ...] is defined as x1 ∨ (x2 ∨ ...), or false if the list is empty.

source

meta def expr.local_binding_info :

expr → binder_info

local_binding_info e returns the binding info of e if e is a local constant. Otherwise returns binder_info.default.

source

meta def expr.is_default_local :

expr → bool

is_default_local e tests whether e is a local constant with binder info binder_info.default

source

meta def expr.has_local_constant (e l : expr) :

bool

has_local_constant e l checks whether local constant l occurs in expression e

source

meta def expr.to_binder :

expr → binder

Turns a local constant into a binder

source

meta def expr.get_local_const_kind :

expr → name × binder_info × expr

Strip-away the context-dependent unique id for the given local const and return: its friendly name, its binder_info, and its type : expr.

source

meta def expr.local_const_set_type {elab : bool} :

expr elab → expr elab → expr elab

local_const_set_type e t sets the type of e to t, if e is a local_const.

source

meta def expr.unsafe_cast {elab₁ elab₂ : bool} :

expr elab₁ → expr elab₂

unsafe_cast e freely changes the elab : bool parameter of the passed expr. Mainly used to access core expr manipulation functions for pexpr-based use, but which are restricted to expr tt at the site of definition unnecessarily.

DANGER: Unless you know exactly what you are doing, this is probably not the function you are looking for. For pexpr → expr see tactic.to_expr. For expr → pexpr see to_pexpr.

source

meta def expr.replace_subexprs {elab : bool} (e : expr elab) (mappings : list (expr × expr)) :

expr elab

replace_subexprs e mappings takes an e : expr and interprets a list (expr × expr) as a collection of rules for variable replacements. A pair (f, t) encodes a rule which says "whenever f is encountered in e verbatim, replace it with t".

source

meta def expr.is_implicitly_included_variable (e : expr) (vs : list expr) :

bool

is_implicitly_included_variable e vs accepts e, an expr.local_const, and a list vs of other expr.local_consts. It determines whether e should be considered "available in context" as a variable by virtue of the fact that the variables vs have been deemed such.

For example, given variables (n : ℕ) [prime n] [ih : even n], a reference to n implies that the typeclass instance prime n should be included, but ih : even n should not.

DANGER: It is possible that for f : expr another expr.local_const, we have is_implicitly_included_variable f vs = ff but is_implicitly_included_variable f (e :: vs) = tt. This means that one usually wants to iteratively add a list of local constants (usually, the variables declared in the local scope) which satisfy is_implicitly_included_variable to an initial vs, repeating if any variables were added in a particular iteration. The function all_implicitly_included_variables below implements this behaviour.

Note that if e ∈ vs then is_implicitly_included_variable e vs = tt.

source

meta def expr.all_implicitly_included_variables (es vs : list expr) :

list expr

all_implicitly_included_variables es vs accepts es, a list of expr.local_const, and vs, another such list. It returns a list of all variables e in es or vs for which an inclusion of the variables in vs into the local context implies that e should also be included. See is_implicitly_included_variable e vs for the details.

In particular, those elements of vs are included automatically.

source

meta def expr.list_explicit_args (f : expr) :

tactic (list expr)

Get the list of explicit arguments of a function.

source

meta def expr.replace_explicit_args (f : expr) (parg : list expr) :

tactic expr

replace_explicit_args f parg assumes that f is an expression corresponding to a function application. It replaces the explicit arguments of f, in succession, by the elements of parg. The implicit arguments of f remain unchanged.

source

@[protected]

meta def expr.simple_infer_type (env : environment) (e : expr) :

exceptional expr

Infer the type of an application of the form f x1 x2 ... xn, where f is an identifier. This also works if x1, ... xn contain free variables.

source

meta def expr.head_eta_expand_aux :

ℕ → expr → expr → expr

Auxilliary function for head_eta_expand.

source

meta def expr.head_eta_expand (n : ℕ) (e t : expr) :

expr

head_eta_expand n e t eta-expands e n times, with the binders info and domains obtained by its type t.

source

@[protected]

meta def expr.eta_expand (env : environment) (dict : name_map (list ℕ)) :

expr → expr

e.eta_expand env dict eta-expands all expressions that have as head a constant n in dict. They are expanded until they are applied to one more argument than the maximum in dict.find n.

source

@[protected]

meta def expr.apply_replacement_fun (f : name → name) (test : expr → bool) (relevant : name_map ℕ) (reorder : name_map (list ℕ)) :

expr → expr

e.apply_replacement_fun f test applies f to each identifier (inductive type, defined function etc) in an expression, unless

The identifier occurs in an application with first argument arg; and
test arg is false. However, if f is in the dictionary relevant, then the argument relevant.find f is tested, instead of the first argument.

Reorder contains the information about what arguments to reorder: e.g. g x₁ x₂ x₃ ... xₙ becomes g x₂ x₁ x₃ ... xₙ if reorder.find g = some [1]. We assume that all functions where we want to reorder arguments are fully applied. This can be done by applying expr.eta_expand first.

source

meta def environment.is_structure (env : environment) (n : name) :

bool

Tests whether n is a structure.

source

meta def environment.structure_fields_full (env : environment) (n : name) :

option (list name)

Get the full names of all projections of the structure n. Returns none if n is not a structure.

source

meta def environment.is_ginductive' (e : environment) (nm : name) :

bool

Tests whether nm is a generalized inductive type that is not a normal inductive type. Note that is_ginductive returns tt even on regular inductive types. This returns tt if nm is (part of a) mutually defined inductive type or a nested inductive type.

source

meta def environment.decl_filter_map {α : Type} (e : environment) (f : declaration → option α) :

list α

For all declarations d where f d = some x this adds x to the returned list.

source

meta def environment.decl_map {α : Type} (e : environment) (f : declaration → α) :

list α

Maps f to all declarations in the environment.

source

meta def environment.get_decls (e : environment) :

list declaration

Lists all declarations in the environment

source

meta def environment.get_trusted_decls (e : environment) :

list declaration

Lists all trusted (non-meta) declarations in the environment

source

meta def environment.get_decl_names (e : environment) :

list name

Lists the name of all declarations in the environment

source

meta def environment.mfold {α : Type} {m : Type → Type} [monad m] (e : environment) (x : α) (fn : declaration → α → m α) :

m α

Fold a monad over all declarations in the environment.

source

meta def environment.filter (e : environment) (test : declaration → bool) :

list declaration

Filters all declarations in the environment.

source

meta def environment.mfilter (e : environment) (test : declaration → tactic bool) :

tactic (list declaration)

Filters all declarations in the environment.

source

meta def environment.is_prefix_of_file (e : environment) (s : string) (n : name) :

bool

Checks whether s is a prefix of the file where n is declared. This is used to check whether n is declared in mathlib, where s is the mathlib directory.

source

meta def expr.is_eta_expansion_of (args : list expr) (univs : list level) (l : list (name × expr)) :

bool

is_eta_expansion_of args univs l checks whether for all elements (nm, pr) in l we have pr = nm.{univs} args. Used in is_eta_expansion, where l consists of the projections and the fields of the value we want to eta-reduce.

source

meta def expr.is_eta_expansion_test :

list (name × expr) → option expr

is_eta_expansion_test l checks whether there is a list of expresions args such that for all elements (nm, pr) in l we have pr = nm args. If so, returns the last element of args. Used in is_eta_expansion, where l consists of the projections and the fields of the value we want to eta-reduce.

source

meta def expr.is_eta_expansion_aux (val : expr) (l : list (name × expr)) :

tactic (option expr)

is_eta_expansion_aux val l checks whether val can be eta-reduced to an expression e. Here l is intended to consists of the projections and the fields of val. This tactic calls is_eta_expansion_test l, but first removes all proofs from the list l and afterward checks whether the resulting expression e unifies with val. This last check is necessary, because val and e might have different types.

source

meta def expr.is_eta_expansion (val : expr) :

tactic (option expr)

is_eta_expansion val checks whether there is an expression e such that val is the eta-expansion of e. With eta-expansion we here mean the eta-expansion of a structure, not of a function. For example, the eta-expansion of x : α × β is ⟨x.1, x.2⟩. This assumes that val is a fully-applied application of the constructor of a structure.

This is useful to reduce expressions generated by the notation { field_1 := _, ..other_structure } If other_structure is itself a field of the structure, then the elaborator will insert an eta-expanded version of other_structure.

source

@[protected]

meta def declaration.update_with_fun (env : environment) (f : name → name) (test : expr → bool) (relevant : name_map ℕ) (reorder : name_map (list ℕ)) (tgt : name) (decl : declaration) :

declaration

declaration.update_with_fun f test tgt decl sets the name of the given decl : declaration to tgt, and applies both expr.eta_expand and expr.apply_replacement_fun to the value and type of decl.

source

meta def declaration.in_current_file (d : declaration) :

tactic bool

Checks whether the declaration is declared in the current file. This is a simple wrapper around environment.in_current_file Use environment.in_current_file instead if performance matters.

source

meta def declaration.is_theorem :

declaration → bool

Checks whether a declaration is a theorem

source

meta def declaration.is_constant :

declaration → bool

Checks whether a declaration is a constant

source

meta def declaration.is_axiom :

declaration → bool

Checks whether a declaration is a axiom

source

meta def declaration.is_auto_generated (e : environment) (d : declaration) :

bool

Checks whether a declaration is automatically generated in the environment. There is no cheap way to check whether a declaration in the namespace of a generalized inductive type is automatically generated, so for now we say that all of them are automatically generated.

source