Major Section: MISCELLANEOUS

Many low-level ACL2 functions take and return ``tag trees'' or ``ttrees'' (pronounced ``tee-trees'') which contain various useful bits of information such as the lemmas used, the linearize assumptions made, etc.

Abstractly a tag-tree represents a list of sets, each member set having a
name given by one of the ``tags'' (which are symbols) of the ttree. The
elements of the set named `tag`

are all of the objects tagged `tag`

in
the tree. You are invited to browse the source code. Definitions of
primitives are labeled with the comment ``; Note: Tag-tree primitive''.

The rewriter, for example, takes a term and a ttree (among other things), and
returns a new term, term', and new ttree, ttree'. Term' is equivalent to
term (under the current assumptions) and the ttree' is an extension of ttree.
If we focus just on the set associated with the tag `LEMMA`

in the ttrees,
then the set for ttree' is the extension of that for ttree obtained by
unioning into it all the runes used by the rewrite. The set associated
with `LEMMA`

can be obtained by `(tagged-objects 'LEMMA ttree)`

.