Print the events named by a logical name
Example: :pe fn ; sketches the command that introduced fn and ; prints in full the event within it that created fn.
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
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.
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!.