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