OTHER

Major Section:  ACL2 Documentation

Some Related Topics

• ACCUMULATED-PERSISTENCE -- to get statistics on which runes are being tried

• ACL2-DEFAULTS-TABLE -- a table specifying certain defaults, e.g., the default defun-mode

• ACL2-HELP -- the acl2-help mailing list

• BREAK$ -- cause an immediate Lisp break

• CERTIFY-BOOK -- how to produce a certificate for a book

• CERTIFY-BOOK! -- a variant of certify-book

• CW-GSTACK -- debug a rewriting loop or stack overflow

• DEAD-EVENTS -- using proof supporters to identify dead code and unused theorems

• DISASSEMBLE$ -- disassemble a function

• DMR -- dynamically monitor rewrites and other prover activity

• DYNAMICALLY-MONITOR-REWRITES -- See dmr.

• EXIT -- quit entirely out of Lisp

• GOOD-BYE -- quit entirely out of Lisp

• GUARD-OBLIGATION -- the guard proof obligation

• IN-PACKAGE -- select current package

• LD -- the ACL2 read-eval-print loop, file loader, and command processor

• PRINT-GV -- print a form whose evaluation caused a guard violation

• PROPS -- print the ACL2 properties on a symbol

• PSO -- show the most recently saved output

• PSO! -- show the most recently saved output, including proof-tree output

• PSOF -- show the most recently saved output

• PSOG -- show the most recently saved output in gag-mode

• PSTACK -- seeing what is the prover up to

• Q -- quit ACL2 (type :q) -- reenter with (lp)

• QUIT -- quit entirely out of Lisp

• REBUILD -- a convenient way to reconstruct your old state

• REDO-FLAT -- redo on failure of a progn, encapsulate, or certify-book

• RESET-LD-SPECIALS -- restores initial settings of the ld specials

• SAVE-EXEC -- save an executable image and (for most Common Lisps) a wrapper script

• SET-ACCUMULATED-PERSISTENCE -- See accumulated-persistence.

• SHARP-BANG-READER -- package prefix that is not restricted to symbols

• SHARP-COMMA-READER -- DEPRECATED read-time evaluation of constants

• SHARP-DOT-READER -- read-time evaluation of constants

• SHARP-U-READER -- allow underscore characters in numbers

• SHOW-ACCUMULATED-PERSISTENCE -- See accumulated-persistence.

• SKIP-PROOFS -- skip proofs for a given form -- a quick way to introduce unsoundness

• STATE -- the von Neumannesque ACL2 state object

• THM -- prove a theorem

• TIME$ -- time an evaluation

• TOP-LEVEL -- evaluate a top-level form as a function body

• TRACE -- tracing functions in ACL2

• TRANS -- print the macroexpansion of a form

• TRANS! -- print the macroexpansion of a form without single-threadedness concerns

• TRANS1 -- print the one-step macroexpansion of a form

• VERIFY-GUARDS-FORMULA -- view the guard proof obligation, without proving it

• WALKABOUT -- explore an ACL2 cons tree

• WITH-PROVER-STEP-LIMIT -- limit the number of steps for proofs

• WITH-PROVER-TIME-LIMIT -- limit the time for proofs

• WOF -- direct standard output and proofs output to a file

This section contains an assortment of top-level functions that fit into none of the other categories and yet are suffiently useful as to merit ``advertisement'' in the :help command.