display the current abbreviations
Major Section: PROOF-CHECKER-COMMANDS
Examples: (show-abbreviations v w) -- assuming that v and w currently abbreviate terms, then this instruction displays them together with the terms they abbreviate show-abbreviations -- display all abbreviationsSee also
add-abbreviation
and remove-abbreviations
. In
particular, the documentation for add-abbreviation
contains a
general discussion of abbreviations.
General Form: (show-abbreviations &rest vars)Display each argument in
vars
together with the term it abbreviates
(if any). If there are no arguments, i.e. the instruction is simply
show-abbreviations
, then display all abbreviations together with the
terms they abbreviate.If the term abbreviated by a variable, say v
, contains a proper
subterm that is also abbreviate by (another) variable, then both the
unabbreviated term and the abbreviated term (but not using (? v)
to
abbreviate the term) are displayed with together with v
.