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 -- associate directory to keyword for include-book's :dir argument

• 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-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

• BINOP-TABLE -- associates binary function with the corresponding macro

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

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

• DELETE-INCLUDE-BOOK-DIR -- remove association of keyword for include-book's :dir argument

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

• 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

• 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 binary 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-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

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

• SET-BACKCHAIN-LIMIT -- Sets the backchain-limit used by the rewriter

• 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-PRINT-CLAUSE-IDS -- cause subgoal numbers to be printed when 'prove output is inhibited

• 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-SAVED-OUTPUT -- save proof output for later display with :pso or :pso!

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

• SET-TAINTED-OK -- See set-tainted-okp.

• SET-TAINTED-OKP -- control output

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

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

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

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

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

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