Nth-aliases-table
A table used to associate names for nth/update-nth printing
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 nth
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.
Subtopics
- Remove-nth-alias
- Remove a symbol alias for printing of nth/update-nth terms
- Add-nth-alias
- Associate one symbol with another for printing of nth/update-nth terms
