		Search-engine friendly clone of the ACL2 documentation.

Mlib

Allexprs

Functions for gathering all the expressions used throughout some module item.

These functions gather up what we regard as the "top level" expressions used throughout various module items. That is, consider an assignment statement such as foo = a + b; the associated list of allexprs would include two expressions: one for foo, and one for a + b.

Note that despite the name "allexprs", we actually do not gather expressions within (* foo = bar *)-style attributes.