• 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
        • 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
    • Proof-builder-commands
    • Proof-builder-commands-short-list

    ACL2-pc::goals

    (macro) list the names of goals on the stack

    Example and General Form:
    goals

    Goals lists the names of all goals that remain to be proved. They are listed in the order in which they appear on the stack of remaining goals, which is relevant for example to the effect of a change-goal instruction.