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

(macro) same as rewrite

Example:
(r 3)

See ACL2-pc::rewrite.