Print the events named by a logical name
:pe fn ; sketches the command that introduced fn and
; prints in full the event within it that created fn.
Pe takes one argument, a logical name, and prints the event
corresponding to the name, doing so in full unless the ld-evisc-tuple
is non-nil, in which case it abbreviates using that evisc-tuple; see evisc-tuple. Pe also sketches the command responsible for that
event if the command is different from the event itself. To remind
you that the event is inferior to the command, i.e., you can only undo
the entire command, not just the event, the event is indented slightly
from the command and a slash (meant to suggest a tree branch) connects
See pc for a description of the format used to display a command.
If the given logical name corresponds to more than one event, then :pe
will print the above information for every such event. Here is an example of
ACL2 !>:pe nth
-4270 (ENCAPSULATE NIL ...)
>V (VERIFY-TERMINATION NTH)
Additional events for the logical name NTH:
PV -4949 (DEFUN NTH (N L)
"Documentation available via :doc"
(DECLARE (XARGS :GUARD (AND (INTEGERP N)
(>= N 0)
(IF (ENDP L)
(IF (ZP N)
(NTH (- N 1) (CDR L)))))
If you prefer to see only the formula for the given name, for example if it
is part of a large mutual-recursion, see pf.
See extend-pe-table for a way to specify a form to be printed in
place of the actual event. To avoid such replacement, see pe!.
- Returns a summary of where a logical-name originates from.