Macros-after
Macro names introduced after a given event name
Evaluate (macros-after NAME), where NAME is a symbol
naming an event in the current ACL2 world, to obtain a list of macro
names introduced after NAME was introduced. That list L has no
duplicates; moreover, for any symbols m1 and m2 in L, m1
occurs before m2 in L if and only if m1 was introduced before
m2 in the current ACL2 world.
To use this tool:
(include-book "tools/names-after" :dir :system)
In a program you can invoke (macros-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
(macros-after NAME) macroexpands to (macros-after-fn 'NAME (w
state)).
See functions-after for an utility to apply to obtain function
symbols.
