• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
        • Instructions
        • Proof-builder-commands
        • Proof-builder-commands-short-list
          • ACL2-pc::=
          • ACL2-pc::s
          • ACL2-pc::exit
          • ACL2-pc::in-theory
          • ACL2-pc::comm
          • ACL2-pc::dv
          • ACL2-pc::x
          • ACL2-pc::show-rewrites
          • ACL2-pc::claim
          • ACL2-pc::split
          • ACL2-pc::prove
          • ACL2-pc::save
          • ACL2-pc::demote
          • ACL2-pc::retrieve
          • ACL2-pc::bash
          • ACL2-pc::p-top
          • ACL2-pc::expand
          • ACL2-pc::bk
          • ACL2-pc::induct
          • ACL2-pc::undo
          • ACL2-pc::top
          • ACL2-pc::restore
          • ACL2-pc::replay
          • ACL2-pc::p
            • ACL2-pc::nx
            • ACL2-pc::contrapose
            • ACL2-pc::up
            • ACL2-pc::th
            • ACL2-pc::use
            • ACL2-pc::s-prop
            • ACL2-pc::runes
            • ACL2-pc::goals
            • ACL2-pc::drop
            • ACL2-pc::x-dumb
            • ACL2-pc::cg
            • ACL2-pc::sr
            • ACL2-pc::r
          • Dive-into-macros-table
          • Verify
          • Define-pc-macro
          • Macro-command
          • Define-pc-help
          • Toggle-pc-macro
          • Define-pc-meta
          • Retrieve
          • Unsave
          • Proof-checker
        • Recursion-and-induction
        • Hons-and-memoization
        • Events
        • Parallelism
        • History
        • Programming
        • Operational-semantics
        • Real
        • Start-here
        • Miscellaneous
        • Output-controls
        • Bdd
        • Macros
        • Installation
        • Mailing-lists
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Proof-builder-commands
    • Proof-builder-commands-short-list

    ACL2-pc::p

    (macro) prettyprint the current term in the usual user-level (untranslated) syntax

    Example and General Form:
p

    Prettyprint the current term. The usual user (untranslated) syntax is used, so that for example one would see (and x y) rather than (if x y 'nil). (See also pp.) Also, abbreviations are inserted where appropriate; see ACL2-pc::add-abbreviation.

    The ``current term'' is the entire conclusion unless dive commands have been given, in which case it may be a subterm of the conclusion.

    If all goals have been proved, a message saying so will be printed (as there will be no current term!).