Functions-after
Function symbols introduced after a given event name
Evaluate (functions-after NAME), where NAME is a symbol
naming an event in the current ACL2 world, to obtain a list of function
symbols introduced after NAME was introduced. That list L has no
duplicates; moreover, for any symbols f1 and f2 in L, f1
occurs before f2 in L if and only if f1 was introduced before
f2 in the current ACL2 world, except that the order is undefined when
f1 and f2 were introduced in the same mutual-recursion
event.
To use this tool:
(include-book "tools/names-after" :dir :system)
In a program you can invoke (functions-after-fn x wrld) on an
expression, x, to obtain the result described above where NAME is
the value of x and wrld is an ACL2 world. In particular, the
call (functions-after NAME) macroexpands to (functions-after-fn
'NAME (w state)).
See macros-after for an utility to apply to obtain macro
names.
