PE

Major Section:  HISTORY

Example:
: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 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) connects them.

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 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 !>