• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
    • Break-rewrite
    • Proof-builder
      • Instructions
      • Proof-builder-commands
        • ACL2-pc::rewrite
        • ACL2-pc::apply-linear
        • ACL2-pc::sequence
        • Proof-builder-commands-short-list
        • ACL2-pc::=
        • ACL2-pc::s
        • ACL2-pc::exit
        • ACL2-pc::type-alist
        • ACL2-pc::in-theory
        • ACL2-pc::equiv
        • ACL2-pc::comm
        • ACL2-pc::casesplit
        • ACL2-pc::add-abbreviation
        • ACL2-pc::dv
          • Dive-into-macros-table
            • Remove-dive-into-macro
            • Add-dive-into-macro
        • ACL2-pc::hyps
        • ACL2-pc::prove-termination
        • ACL2-pc::prove-guard
        • ACL2-pc::x
        • ACL2-pc::pot-lst
        • ACL2-pc::fancy-use
        • ACL2-pc::dive
        • ACL2-pc::generalize
        • ACL2-pc::lisp
        • ACL2-pc::show-rewrites
        • ACL2-pc::claim
        • ACL2-pc::put
        • ACL2-pc::split
        • ACL2-pc::geneqv
        • ACL2-pc::prove
        • ACL2-pc::help
        • ACL2-pc::save
        • ACL2-pc::do-all
        • ACL2-pc::demote
        • ACL2-pc::wrap1
        • ACL2-pc::show-abbreviations
        • ACL2-pc::promote
        • ACL2-pc::retrieve
        • ACL2-pc::reduce
        • ACL2-pc::forwardchain
        • ACL2-pc::doc
        • ACL2-pc::bash
        • ACL2-pc::p-top
        • ACL2-pc::print
        • ACL2-pc::expand
        • ACL2-pc::bk
        • ACL2-pc::wrap
        • ACL2-pc::remove-abbreviations
        • ACL2-pc::reduce-by-induction
        • ACL2-pc::induct
        • ACL2-pc::unsave
        • ACL2-pc::undo
        • ACL2-pc::top
        • ACL2-pc::restore
        • ACL2-pc::replay
        • ACL2-pc::psog
        • ACL2-pc::p
        • ACL2-pc::nx
        • ACL2-pc::noise
        • ACL2-pc::contrapose
        • ACL2-pc::wrap-induct
        • ACL2-pc::pso!
        • ACL2-pc::pso
        • ACL2-pc::up
        • ACL2-pc::then
        • ACL2-pc::th
        • ACL2-pc::sl
        • ACL2-pc::show-type-prescriptions
        • ACL2-pc::bdd
        • ACL2-pc::repeat
        • ACL2-pc::pr
        • ACL2-pc::pl
        • ACL2-pc::finish
        • ACL2-pc::commands
        • ACL2-pc::change-goal
        • ACL2-pc::use
        • ACL2-pc::show-linears
        • ACL2-pc::s-prop
        • ACL2-pc::runes
        • ACL2-pc::protect
        • ACL2-pc::instantiate
        • ACL2-pc::insist-all-proved
        • ACL2-pc::fail
        • ACL2-pc::clause-processor
        • ACL2-pc::bookmark
        • ACL2-pc::retain
        • ACL2-pc::quiet!
        • ACL2-pc::pro
        • ACL2-pc::orelse
        • ACL2-pc::goals
        • ACL2-pc::drop
        • ACL2-pc::do-strict
        • ACL2-pc::print-all-concs
        • ACL2-pc::do-all-no-prompt
        • ACL2-pc::x-dumb
        • ACL2-pc::succeed
        • ACL2-pc::print-all-goals
        • ACL2-pc::pp
        • ACL2-pc::noise!
        • ACL2-pc::nil
        • ACL2-pc::negate
        • ACL2-pc::illegal
        • ACL2-pc::elim
        • ACL2-pc::sls
        • ACL2-pc::quiet
        • ACL2-pc::claim-simple
        • ACL2-pc::cg
        • ACL2-pc::pro-or-skip
        • ACL2-pc::ex
        • ACL2-pc::comment
        • ACL2-pc::ACL2-wrap
        • ACL2-pc::when-not-proved
        • ACL2-pc::skip
        • ACL2-pc::retain-or-skip
        • ACL2-pc::repeat-until-done
        • ACL2-pc::free
        • ACL2-pc::drop-or-skip
        • ACL2-pc::cg-or-skip
        • ACL2-pc::by
        • ACL2-pc::split-in-theory
        • ACL2-pc::st
        • ACL2-pc::sr
        • ACL2-pc::print-main
        • ACL2-pc::lemmas-used
        • ACL2-pc::cl-proc
        • ACL2-pc::al
        • ACL2-pc::run-instr-on-new-goals
        • ACL2-pc::run-instr-on-goal
        • ACL2-pc::repeat-rec
        • ACL2-pc::r
        • ACL2-pc::contradict
      • Proof-builder-commands-short-list
      • Dive-into-macros-table
        • Remove-dive-into-macro
        • Add-dive-into-macro
      • 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
    • Guard-debug
    • Set-debugger-enable
    • 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
    • Prettygoals
    • 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
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Dive-into-macros-table

Add-dive-into-macro

Associate proof-builder diving function with macro name

Examples:
(add-dive-into-macro cat expand-address-cat)

This feature is used so that the interactive proof-builder's DV command and numeric diving commands (e.g., 3) will dive properly into subterms. Please see dive-into-macros-table.