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

    (meta) undo some instructions

    Examples:
    (undo 7)
    undo
    
    General Forms:
    
    (undo n) -- Undo the last n instructions.  The argument n should be
                a positive integer.
    
    undo     -- Same as (undo 1).

    Remark: To remove the effect of an undo command, use restore; see ACL2-pc::restore.

    Remark: If the argument n is greater than the total number of interactive instructions in the current session, then (undo n) will simply take you back to the start of the session.

    The undo meta command always ``succeeds''; it returns (mv nil t state) unless its optional argument is supplied and of the wrong type (i.e. not a positive integer) or there are no instructions to undo.