• 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
        • Pl
        • Command
        • Puff
        • Pc
        • Ld-history
        • Oops
        • Extend-pe-table
        • Ubt
        • Puff*
        • Ubi
        • Pe
        • Undo
          • Ubt
          • Ubu
          • Ubt!
          • U
          • Ubu!
            • Ubu?
            • Ubt?
            • Ubt-prehistory
          • Make-termination-theorem
          • Command-descriptor
          • Reset-prehistory
          • Gthm
          • Formula
          • Pr
          • Pcb
          • Ubu
          • Disable-ubt
          • Pl2
          • Pbt
          • Enter-boot-strap-mode
          • Reset-kill-ring
          • Ubt!
          • U
          • Tthm
          • Pf
          • Ubu!
            • Pr!
            • Pcs
            • Pcb!
            • Get-command-sequence
            • Exit-boot-strap-mode
            • Ubu?
            • Ubt?
            • Ep-
            • Ubt-prehistory
            • Tau-database
            • Ep
            • Pe!
          • Programming
          • Operational-semantics
          • Real
          • Start-here
          • Debugging
          • Miscellaneous
          • Output-controls
          • Macros
          • Interfacing-tools
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • History
      • Undo

      Ubu!

      Undo commands, without a query or an error

      See undo for an introduction to undoing commands.

      Example:
      :ubu! :x-4

      The keyword command :ubu! is the same as :ubu, but with a guarantee that it is ``error-free.'' More precisely, the error-triple returned by :ubu! will always be of the form (mv nil val state). Note that :ubu! will not print error messages.

      :Oops will undo the last :ubu!. Also see ubu, ubu?, ubt, ubt!, ubt?, and u.