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