		Search-engine friendly clone of the ACL2 documentation.

History

Pe

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 logical-name.

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 them.

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

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

Subtopics

Origin: Returns a summary of where a logical-name originates from.