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

    (macro) replay one or more instructions

    Examples:
    REPLAY     -- replay all instructions in the current session
                  (i.e., state-stack)
    (REPLAY 5) -- replay the most recent 5 instructions
    (REPLAY 5
            (COMMENT deleted dive command here))
               -- replace the 5th most recent instruction with the
                  indicated comment instruction, and then replay it
                  followed by the remaining 4 instructions
    
    General Form:
    (REPLAY &OPTIONAL n replacement-instruction)

    Replay the last n instructions if n is a positive integer; else n should be nil or not supplied, and replay all instructions. However, if replacement-instruction is supplied and not nil, then before the replay, replace the nth instruction (from the most recent, as shown by commands) with replacement-instruction.

    If this command ``fails'', then the restore command will revert the state-stack to its value present before the replay instruction was executed.