• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Hons-and-memoization
      • Events
      • History
      • Parallelism
      • Programming
      • Start-here
      • Real
      • Debugging
      • Miscellaneous
        • Term
        • Ld
          • Wormhole
          • Ld-skip-proofsp
          • Ld-redefinition-action
          • Lp
          • Ld-error-action
          • Ld-history
          • Guarantees-of-the-top-level-loop
          • Ld-post-eval-print
          • Ld-keyword-aliases
          • Current-package
          • Ld-query-control-alist
          • Ld-prompt
          • Keyword-commands
          • Redef+
          • Rebuild
          • Prompt
          • Ld-pre-eval-print
          • Calling-ld-in-bad-contexts
          • Ld-pre-eval-filter
          • P!
          • Ld-error-triples
          • Ld-verbose
          • Ld-evisc-tuple
          • A!
          • Default-print-prompt
            • Reset-ld-specials
            • Ld-always-skip-top-level-locals
            • Ld-missing-input-ok
            • Redef
            • Redef!
            • Redef-
            • I-am-here
            • Abort!
          • Hints
          • Type-set
          • Ordinals
          • ACL2-customization
          • With-prover-step-limit
          • With-prover-time-limit
          • Set-prover-step-limit
          • Local-incompatibility
          • Set-case-split-limitations
          • Subversive-recursions
          • Specious-simplification
          • Defsum
          • Oracle-timelimit
          • Thm
          • Defopener
          • Gcl
          • Case-split-limitations
          • Set-gc-strategy
          • Default-defun-mode
          • Top-level
          • Reader
          • Ttags-seen
          • Adviser
          • Ttree
          • Abort-soft
          • Defsums
          • Gc$
          • With-timeout
          • Coi-debug::fail
          • Expander
          • Gc-strategy
          • Coi-debug::assert
          • Sin-cos
          • Def::doc
          • Syntax
          • Subversive-inductions
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Ld

    Default-print-prompt

    The default prompt printed by ld

    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>