|
|
|---|
|
|
|
|---|
Tag-trees
Many low-level ACL2 functions take and return ``tag trees'' or
``ttrees'' (pronounced ``tee-trees'') which contain useful information such as
the lemmas used, the linearize assumptions made, etc. Here we present only
minimal user-level information, for example in support of the use of the break-rewrite utility or writing metafunctions. Implementation-level
information about tag trees may be found in the Developer's Guide; users
should probably not visit
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
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