SWITCHES-PARAMETERS-AND-MODES

Major Section:  ACL2 Documentation

The beginning user might pay special attention to documentation for logic and program. Other topics in this section can be read as one gains familiarity with ACL2.

Some Related Topics

• ACL2-CUSTOMIZATION -- file of initial commands for ACL2 to run at startup

• ADD-BINOP -- associate a function name with a macro name

• ADD-DEFAULT-HINTS -- add to the default hints

• ADD-DEFAULT-HINTS! -- add to the default hints non-locally

• ADD-DIVE-INTO-MACRO -- associate proof-checker diving function with macro name

• ADD-INCLUDE-BOOK-DIR -- link keyword for :dir argument of ld and include-book

• ADD-INVISIBLE-FNS -- make some unary functions invisible to the loop-stopper algorithm

• ADD-MACRO-ALIAS -- associate a function name with a macro name

• ADD-MACRO-FN -- associate a function name with a macro name

• ADD-MATCH-FREE-OVERRIDE -- set :match-free value to :once or :all in existing rules

• ADD-NTH-ALIAS -- associate one symbol with another for printing of nth/update-nth terms

• ADD-OVERRIDE-HINTS -- add to the override-hints

• ADD-OVERRIDE-HINTS! -- add non-locally to the override-hints

• DEFAULT-HINTS-TABLE -- a table used to provide hints for proofs

• DEFAULT-VERIFY-GUARDS-EAGERNESS -- See set-verify-guards-eagerness.

• DELETE-INCLUDE-BOOK-DIR -- unlink keyword for :dir argument of ld and include-book

• DIVE-INTO-MACROS-TABLE -- right-associated function information for the proof-checker

• FINALIZE-EVENT-USER -- user-supplied code to complete events, e.g., with extra summary output

• INITIALIZE-EVENT-USER -- user-supplied code to initiate events

• INVISIBLE-FNS-TABLE -- functions that are invisible to the loop-stopper algorithm

• LOGIC -- to set the default defun-mode to :logic

• MACRO-ALIASES-TABLE -- a table used to associate function names with macro names

• NTH-ALIASES-TABLE -- a table used to associate names for nth/update-nth printing

• PRINT-SUMMARY-USER -- See finalize-event-user.

• PROGRAM -- to set the default defun-mode to :program

• PUSH-UNTOUCHABLE -- add name or list of names to the list of untouchable symbols

• REMOVE-BINOP -- remove the association of a function name with a macro name

• REMOVE-DEFAULT-HINTS -- remove from the default hints

• REMOVE-DEFAULT-HINTS! -- remove from the default hints non-locally

• REMOVE-DIVE-INTO-MACRO -- removes association of proof-checker diving function with macro name

• REMOVE-INVISIBLE-FNS -- make some unary functions no longer invisible

• REMOVE-MACRO-ALIAS -- remove the association of a function name with a macro name

• REMOVE-MACRO-FN -- remove the association of a function name with a macro name

• REMOVE-NTH-ALIAS -- remove a symbol alias for printing of nth/update-nth terms

• REMOVE-OVERRIDE-HINTS -- delete from the list of override-hints

• REMOVE-OVERRIDE-HINTS! -- delete non-locally from the list of override-hints

• REMOVE-UNTOUCHABLE -- remove names from lists of untouchable symbols

• RESET-PREHISTORY -- reset the prehistory

• RETURN-LAST-TABLE -- install special raw Lisp behavior

• RULER-EXTENDERS -- control for ACL2's termination and induction analyses

• SET-ABSSTOBJ-DEBUG -- obtain debugging information upon atomicity violation for an abstract stobj

• SET-BACKCHAIN-LIMIT -- sets the backchain-limit used by the type-set and rewriting mechanisms

• SET-BOGUS-DEFUN-HINTS-OK -- allow unnecessary ``mutual recursion''

• SET-BOGUS-MUTUAL-RECURSION-OK -- allow unnecessary ``mutual recursion''

• SET-CASE-SPLIT-LIMITATIONS -- set the case-split-limitations

• SET-CHECKPOINT-SUMMARY-LIMIT -- control printing of key checkpoints upon a proof's failure

• SET-COMPILE-FNS -- have each function compiled as you go along.

• SET-COMPILER-ENABLED -- See compilation.

• SET-DEBUGGER-ENABLE -- control whether Lisp errors and breaks invoke the Lisp debugger

• SET-DEFAULT-BACKCHAIN-LIMIT -- sets the default backchain-limit used when admitting a rule

• SET-DEFAULT-HINTS -- set the default hints

• SET-DEFAULT-HINTS! -- set the default hints non-locally

• SET-DEFERRED-TTAG-NOTES -- modify the verbosity of TTAG NOTE printing

• SET-ENFORCE-REDUNDANCY -- require most events to be redundant

• SET-GAG-MODE -- modify the nature of proof output

• SET-GUARD-CHECKING -- control checking guards during execution of top-level forms

• SET-IGNORE-DOC-STRING-ERROR -- allow ill-formed documentation strings

• SET-IGNORE-OK -- allow unused formals and locals without an ignore or ignorable declaration

• SET-INHIBIT-OUTPUT-LST -- control output

• SET-INHIBIT-WARNINGS -- control warnings

• SET-INHIBITED-SUMMARY-TYPES -- control which parts of the summary are printed

• SET-INVISIBLE-FNS-TABLE -- set the invisible functions table

• SET-IRRELEVANT-FORMALS-OK -- allow irrelevant formals in definitions

• SET-LD-KEYWORD-ALIASES -- See ld-keyword-aliases.

• SET-LD-REDEFINITION-ACTION -- See ld-redefinition-action.

• SET-LD-SKIP-PROOFS -- See set-ld-skip-proofsp.

• SET-LD-SKIP-PROOFSP -- See ld-skip-proofsp.

• SET-LET*-ABSTRACTION -- See set-let*-abstractionp.

• SET-LET*-ABSTRACTIONP -- to shorten many prettyprinted clauses

• SET-MATCH-FREE-DEFAULT -- provide default for :match-free in future rules

• SET-MATCH-FREE-ERROR -- control error vs. warning when :match-free is missing

• SET-MEASURE-FUNCTION -- set the default measure function symbol

• SET-NON-LINEAR -- See set-non-linearp.

• SET-NON-LINEARP -- to turn on or off non-linear arithmetic reasoning

• SET-NU-REWRITER-MODE -- to turn on and off the nu-rewriter

• SET-OVERRIDE-HINTS -- set the override-hints

• SET-OVERRIDE-HINTS! -- set the override-hints non-locally

• SET-PARALLEL-EXECUTION -- for ACL2(p): enabling parallel execution for four parallelism primitives

• SET-PRINT-CLAUSE-IDS -- cause subgoal numbers to be printed when 'prove output is inhibited

• SET-PROVER-STEP-LIMIT -- sets the step-limit used by the ACL2 prover

• SET-RAW-MODE -- enter or exit ``raw mode,'' a raw Lisp environment

• SET-RAW-MODE-ON! -- enter ``raw mode,'' a raw Lisp environment

• SET-RAW-PROOF-FORMAT -- print runes as lists in proof output from simplification

• SET-REWRITE-STACK-LIMIT -- Sets the rewrite stack depth used by the rewriter

• SET-RULER-EXTENDERS -- See ruler-extenders.

• SET-RW-CACHE-STATE -- set the default rw-cache-state

• SET-RW-CACHE-STATE! -- set the default rw-cache-state non-locally

• SET-SAVED-OUTPUT -- save proof output for later display with :pso or :pso!

• SET-SPLITTER-OUTPUT -- turn on or off reporting of rules that may have caused case splits

• SET-STATE-OK -- allow the use of STATE as a formal parameter

• SET-TAU-AUTO-MODE -- turn on or off automatic (``greedy'') generation of :tau-system rules

• SET-TOTAL-PARALLELISM-WORK-LIMIT -- for ACL2(p): set thread limit for parallelism primitives

• SET-TOTAL-PARALLELISM-WORK-LIMIT-ERROR -- for ACL2(p): control the action taken when the thread limit is exceeded

• SET-VERIFY-GUARDS-EAGERNESS -- the eagerness with which guard verification is tried.

• SET-WATERFALL-PARALLELISM -- for ACL2(p): configuring the parallel execution of the waterfall

• SET-WATERFALL-PARALLELISM-HACKS-ENABLED -- for ACL2(p): enable waterfall-parallelism hacks

• SET-WATERFALL-PARALLELISM-HACKS-ENABLED! -- for ACL2(p): enabling waterfall parallelism hacks

• SET-WATERFALL-PRINTING -- for ACL2(p): configuring the printing that occurs within the parallelized waterfall

• SET-WELL-FOUNDED-RELATION -- set the default well-founded relation

• SET-WRITE-ACL2X -- cause certify-book to write out a .acl2x file

• TAU-STATUS -- query or set tau system status

• TERM-TABLE -- a table used to validate meta rules

• UNTRANS-TABLE -- associates a function symbol with a macro for printing user-level terms

• USER-DEFINED-FUNCTIONS-TABLE -- an advanced table used to replace certain system functions

• VERIFY-GUARDS-EAGERNESS -- See set-verify-guards-eagerness.

• WITH-GUARD-CHECKING -- suppressing or enable guard-checking for a form

• WITH-OUTPUT -- suppressing or turning on specified output for an event