		Search-engine friendly clone of the ACL2 documentation.

Developers-guide

Developers-guide-miscellany

Miscellaneous Information

The initial version of this chapter is little more than a stub. It will probably always benefit from expansion to cover more topics.

Trust tags

See defttag for user-level information about trust tags. The ``Essay on Trust Tags (Ttags)'' provides a lot of relevant background on trust tags at the implementation level. A particularly important point to be emphasized here is the following: The critical aspect of trust tags is that whenever a trust tag is activated, the string "TTAG NOTE" must be printed to *standard-co* (see the definition of print-ttag-note), with the exception that if ttag notes are deferred then initially, only the first such is printed; see set-deferred-ttag-notes. The paper ``Hacking and Extending ACL2'' from the 2007 ACL2 Workshop may be helpful.

Fixnums

In general, Common Lisp computations with numbers are much faster when they only deal with ``small'' numbers called fixnums. See the ``Essay on Fixnum Declarations'' for information about fixnums and ACL2, including a description of the ranges for 32-bit fixnums in different Common Lisp implementations as of this writing. There may be some opportunities made available by modern Lisps that have 64-bit implementations. (CMUCL seems to be an exception.)

NEXT SECTION: developers-guide-releases