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

get_nth_prefix nm n removes the last n components from nm

Pops the top n prefixes from the given name.

Pop the prefix of a 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.

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

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

Get the last component of a name, and convert it to a string.

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.

Appends ' to the end of a name.

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

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

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

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

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

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

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

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

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.

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.

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

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.

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.

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

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.

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

Clean an expression by removing ids listed in clean_ids.

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

Implementation of expr.mreplace.

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.

Match a variable.

Match a sort.

Match a constant.

Match a metavariable.

Match a local constant.

Match an application.

Match an application of coe_fn.

Match an abstraction.

Match a Π type.

Match a let.

Match a macro.

Tests whether an expression is a meta-variable.

Tests whether an expression is a sort.

Get the universe levels of a const expression

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

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.

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.

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

Returns the set of all local constants in an expression.

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

Returns a name_set of all constants in an expression.

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

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

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

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

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

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

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

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

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

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.

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

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

head-reduce a single let expression

head-reduce all let expressions

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

Repeatedly apply expr.subst.

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.

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

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

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

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

Auxiliary defintion for get_app_fn_args.

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

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

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

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

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

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

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

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

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

Turns a local constant into a binder

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

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

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.

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".

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.

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.

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.

Auxilliary function for head_eta_expand.

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

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.

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.

Tests whether n is a structure.

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

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.

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

Maps f to all declarations in the environment.

Lists all declarations in the environment

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

Lists the name of all declarations in the environment

Fold a monad over all declarations in the environment.

Filters all declarations in the environment.

Filters all declarations in the environment.

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.

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.

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.

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.

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.

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.

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.

Checks whether a declaration is a theorem

Checks whether a declaration is a constant

Checks whether a declaration is a axiom

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.

Returns true iff d is an automatically-generated or internal declaration.

Returns the list of universe levels of a declaration.

Returns the reducibility_hints field of a defn, and reducibility_hints.opaque otherwise

pretty-prints a declaration object.