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