This file defines basic operations on the types expr, name, declaration, level, environment.
This file is mostly for non-tactics. Tactics should generally be placed in tactic.core.
expr, name, declaration, level, environment, meta, metaprogramming, tactic
The brackets corresponding to a given binder_info.
Find the largest prefix n of a name such that f n ≠ none, then replace this prefix with the value of f n.
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
Auxilliary definition for pop_nth_prefix
Pops the top n prefixes from the given name.
Pop the prefix of a name
Auxilliary definition for from_components
Build a name from components. For example from_components ["foo","bar"] becomes `foo.bar
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.
Append a string to the last component of a name
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.
Checks whether nm has a prefix (including itself) such that P is true
Appends ' to the end of a name.
Tests whether a universe level is non-zero for all assignments of its variables
The type of binders containing a name, the binding info and the binding type
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.
Turns an expression into a positive natural number, assuming it is only built up from has_one.one, bit0 and bit1.
Turns an expression into a natural number, assuming it is only built up from has_one.one, bit0, bit1 and has_zero.zero.
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.
Apply a function to each constant (inductive type, defined function etc) in an expression.
Tests whether an expression is a meta-variable.
Tests whether an expression is a sort.
If e is a local constant, to_implicit e changes the binder info of e to implicit.
Returns a list of all local constants in an expression (without duplicates).
Returns a name_set of all constants in an expression.
Returns a list of all meta-variables in an expression (without duplicates).
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
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.
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.
Auxilliary definition for expr.pi_arity
The arity of a pi-type. Does not perform any reduction of the expression. In one application this was ~30 times quicker than tactic.get_pi_arity.
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.
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.
Get the codomain/target of a pi-type. This definition doesn't Instantiate bound variables, and therefore produces a term that is open.
Auxilliary defintion for pi_binders.
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
Auxilliary 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.
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
Tests whether a name is declared in the current file. Fixes an error in in_current_file which returns tt for the four names quot, quot.mk, quot.lift, quot.ind
Tests whether n is an inductive type with one constructor without indices. If so, returns the number of paramaters and the name of the constructor. Otherwise, returns none.
Tests whether n is a structure. It will first test whether n is structure-like and then test that the first projection is defined in the environment and is a projection.
Get all projections of the structure n. Returns none if n is not structure-like. If n is not a structure, but is structure-like, this does not check whether the names are existing declarations.
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.
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 retulting 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.
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 the list of universe levels of a declaration.