DEFAULT-PRINT-PROMPT

the default prompt printed by ld 
Major Section:  MISCELLANEOUS


Example prompt:
ACL2 p!s>
The prompt printed by ACL2 displays the current package, followed by a space, followed by zero or more of the three characters as specified below, followed by the character > printed one or more times, reflecting the number of recursive calls of ld. The three characters in the middle are as follows: 
p     ; when (default-defun-mode (w state)) is :program
!     ; when guard checking is on
s     ; when (ld-skip-proofsp state) is t
See default-defun-mode, see set-guard-checking, and see ld-skip-proofsp.

Also see ld-prompt to see how to install your own prompt.

Here are some examples with ld-skip-proofsp nil. 

ACL2 !>    ; logic mode with guard checking on
ACL2 >     ; logic mode with guard checking off
ACL2 p!>   ; program mode with guard checking on
ACL2 p>    ; program mode with guard checking off
Here are some examples with default-defun-mode of :logic. 
ACL2 >     ; guard checking off, ld-skip-proofsp nil
ACL2 s>    ; guard checking off, ld-skip-proofsp t
ACL2 !>    ; guard checking on, ld-skip-proofsp nil
ACL2 !s>   ; guard checking on, ld-skip-proofsp t
Finally, here is the prompt in raw mode (see set-raw-mode), regardless of the settings above: 
ACL2 P>