• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • 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
          • 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
          • 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::x-dumb

    (atomic macro) expand function call at the current subterm, without simplifying

    General Form:
x-dumb:  expand without simplification.

    Same as (expand t). See ACL2-pc::expand.

    Also see ACL2-pc::x, which performs simplification.