Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Break-rewrite
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
Accumulated-persistence
Cgen
Forward-chaining-reports
Proof-tree
Print-gv
Dmr
With-brr-data
Splitter
Set-debugger-enable
Guard-debug
Redo-flat
Time-tracker
Set-check-invariant-risk
Removable-runes
Efficiency
Explain-near-miss
Tail-biting
Failed-forcing
Sneaky
Invariant-risk
Failure
Measure-debug
Dead-events
Compare-objects
Remove-hyps
Type-prescription-debugging
Pstack
Trace
Set-register-invariant-risk
Walkabout
Disassemble$
Nil-goal
Cw-gstack
Set-guard-msg
Find-lemmas
Watch
Quick-and-dirty-subsumption-replacement-step
Profile-all
Profile-ACL2
Set-print-gv-defaults
Minimal-runes
Spacewalk
Try-gl-concls
Near-misses
Std
Proof-automation
Macro-libraries
ACL2
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
.