Additional operations on expr and related types #
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
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
append_to_last nm s is_prefix adds
s to the last component of
either as prefix or as suffix (specified by
is_prefix), separated by
nm has a prefix (including itself) such that P is true
last_string n returns the rightmost component of
n, ignoring numeral components.
last_string `a.b.c.33 will return
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
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.
name.is_likely_generated_binder_name checks if
a name is of the form
Converting between expressions and numerals #
There are a number of ways to convert between expressions and numerals, depending on the input and output types and whether you want to infer the necessary type classes.
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
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
mk_local_pis (when applied to the type of all imported declarations 100x).
In this section we define the tactic
is_eta_expansion which checks whether an expression
is an eta-expansion of a structure. (not to be confused with eta-expanion for