Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
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
Debugging
Miscellaneous
Output-controls
Macros
Interfacing-tools
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
.