Major Section: SWITCHES-PARAMETERS-AND-MODES
Example: (table nth-aliases-table 'st0 'st)This example associates the symbol
st0
with the symbol st
. As a
result, when the theorem prover prints terms of the form
(nth n st0)
or (update-nth n val st0)
, where st
is a stobj
whose n
th accessor function is f-n
, then it will print n
as
*f-n*
.
General Form: (table nth-aliases-table 'alias-name 'name)This event causes
alias-name
to be treated like name
for purposes
of the printing of terms that are calls of nth
and update-nth
.
(Note however that name
is not recursively looked up in this
table.) Both must be symbols other than state
. See term, in
particular the discussion there of untranslated terms.For a convenient way to add entries to this table, see add-nth-alias. To remove entries from the table with ease, see remove-nth-alias.