• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • 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
        • P!
        • Ld-pre-eval-filter
        • Ld-error-triples
        • Ld-evisc-tuple
        • Ld-verbose
        • 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
      • Clause
      • ACL2-customization
      • With-prover-step-limit
      • Set-prover-step-limit
      • With-prover-time-limit
      • Local-incompatibility
      • Set-case-split-limitations
      • Subversive-recursions
      • Specious-simplification
      • Defsum
      • Gcl
      • Oracle-timelimit
      • Thm
      • Defopener
      • 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
  • Math
  • Testing-utilities

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