Major Section: HISTORY
Example: :pe fn ; sketches the command that introduced fn and ; prints in full the event within it that created fn.See logical-name.
Pe takes one argument, a logical name, and prints in full the event
corresponding to the name.
Pe also sketches the command responsible
for that event if the command is different from the event itself.
See pc for a description of the format used to display a command. 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)
If the given logical name corresponds to more than one event, then
will print the above information for every such event. Here is an
example of such behavior.
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) (TRUE-LISTP L)))) (IF (ENDP L) NIL (IF (ZP N) (CAR L) (NTH (- N 1) (CDR L))))) ACL2 !>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.