PE

print the events named by a logical name
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) 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 !>
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.