MISCELLANEOUS

a miscellany of documented functions and concepts (often cited in more accessible documentation)

Major Section: ACL2 Documentation

Some Related Topics

• &ALLOW-OTHER-KEYS -- See macro-args.

• &BODY -- See macro-args.

• &KEY -- See macro-args.

• &OPTIONAL -- See macro-args.

• &REST -- See macro-args.

• &WHOLE -- See macro-args.

• A! -- to return to the top-level of ACL2's command loop

• ABORT! -- to return to the top-level of ACL2's command loop

• ACKNOWLEDGMENTS -- some contributors to the well-being of ACL2

• ACL2S -- See acl2-sedan.

• APROPOS -- searching the documentation online

• BACKCHAIN-LIMIT -- limiting the effort expended on relieving hypotheses

• BACKCHAIN-LIMIT-RW -- hints keyword :BACKCHAIN-LIMIT-RW

• BACKTRACK -- hints keyword :BACKTRACK

• BIBLIOGRAPHY -- reports about ACL2

• BIND-FREE -- to bind free variables of a rewrite or linear rule

• BY -- hints keyword :BY

• CASE-SPLIT -- like force but immediately splits the top-level goal on the hypothesis

• CASE-SPLIT-LIMITATIONS -- a list of two ``numbers'' limiting the number of cases produced at once

• CASES -- hints keyword :CASES

• CLAUSE-IDENTIFIER -- the internal form of a goal-spec

• COMMAND -- forms you type at the top-level, but...

• COMMAND-DESCRIPTOR -- an object describing a particular command typed by the user

• COMMON-LISP -- relation to Common Lisp, including deviations from the spec

• COMPUTED-HINTS -- computing advice to the theorem proving process

• CONSTRAINT -- restrictions on certain functions introduced in encapsulate events

• COPYRIGHT -- ACL2 copyright, license, sponsorship

• COROLLARY -- the corollary formula of a rune

• CURRENT-PACKAGE -- the package used for reading and printing

• CUSTOM-KEYWORD-HINTS -- user-defined hints

• DEFAULT-BACKCHAIN-LIMIT -- specifying the backchain limit for a rule

• DEFAULT-DEFUN-MODE -- the default defun-mode of defun 'd functions

• DEFAULT-HINTS -- a list of hints added to every proof attempt

• DEFAULT-PRINT-PROMPT -- the default prompt printed by ld

• DEFAULT-RULER-EXTENDERS -- the default ruler-extenders for defun 'd functions

• DEFUN-MODE -- determines whether a function definition is a logical act

• DEFUNS -- an alternative to mutual-recursion

• DISABLE-FORCING -- to disallow force d case-split s

• DISABLE-IMMEDIATE-FORCE-MODEP -- forced hypotheses are not attacked immediately

• DISABLEDP -- determine whether a given name or rune is disabled

• DO-NOT -- hints keyword :DO-NOT

• DO-NOT-INDUCT -- hints keyword :DO-NOT-INDUCT

• DOUBLE-REWRITE -- cause a term to be rewritten twice

• EMBEDDED-EVENT-FORM -- forms that may be embedded in other events

• ENABLE-FORCING -- to allow force d split s

• ENABLE-IMMEDIATE-FORCE-MODEP -- forced hypotheses are attacked immediately

• ENTER-BOOT-STRAP-MODE -- The first millisecond of the Big Bang

• ESCAPE-TO-COMMON-LISP -- escaping to Common Lisp

• EXECUTABLE-COUNTERPART -- a rule for computing the value of a function

• EXIT-BOOT-STRAP-MODE -- the end of pre-history

• EXPAND -- hints keyword :EXPAND

• EXTENDED-METAFUNCTIONS -- state and context sensitive metafunctions

• FAILED-FORCING -- how to deal with a proof failure in a forcing round

• FAILURE -- how to deal with a proof failure

• FIND-RULES-OF-RUNE -- find the rules named rune

• FORCE -- identity function used to force a hypothesis

• FORCED -- See force.

• FORCING-ROUND -- a section of a proof dealing with forced assumptions

• FUNCTIONAL-INSTANTIATION-IN-ACL2R -- additional requirements for :functional-instance hints in ACL2(r)

• GAG-MODE -- verbosity of proof output

• GC$ -- invoke the garbage collector

• GC-VERBOSE -- control printing from the garbage collector

• GCL -- tips on building and using ACL2 based on Gnu Common Lisp

• GET-WORMHOLE-STATUS -- make a wormhole's status visible outside the wormhole

• GOAL-SPEC -- to indicate where a hint is to be used

• GUARD -- restricting the domain of a function

• GUARD-HINTS -- xargs keyword :GUARD-HINTS

• HANDS-OFF -- hints keyword :HANDS-OFF

• HIDE -- hide a term from the rewriter

• HINTS -- advice to the theorem proving process

• HINTS-AND-THE-WATERFALL -- how hints fit into the ACL2 proof waterfall

• I-AM-HERE -- a convenient marker for use with rebuild

• IF-INTRO -- See splitter.

• IMMED-FORCED -- See splitter.

• IMMEDIATE-FORCE-MODEP -- when executable counterpart is enabled,
  forced hypotheses are attacked immediately

• INDUCT -- hints keyword :INDUCT

• KEYWORD -- See keywordp.

• KEYWORD-COMMANDS -- how keyword commands are processed

• LAMBDA -- See term.

• LD-ERROR-ACTION -- determines ld 's response to an error

• LD-ERROR-TRIPLES -- determines whether a form caused an error during ld

• LD-EVISC-TUPLE -- determines whether ld suppresses details when printing

• LD-KEYWORD-ALIASES -- allows the abbreviation of some keyword commands

• LD-POST-EVAL-PRINT -- determines whether and how ld prints the result of evaluation

• LD-PRE-EVAL-FILTER -- determines which forms ld evaluates

• LD-PRE-EVAL-PRINT -- determines whether ld prints the forms to be eval'd

• LD-PROMPT -- determines the prompt printed by ld

• LD-QUERY-CONTROL-ALIST -- how to default answers to queries

• LD-REDEFINITION-ACTION -- to allow redefinition without undoing

• LD-SKIP-PROOFSP -- how carefully ACL2 processes your commands

• LD-VERBOSE -- determines whether ld prints ``ACL2 Loading ...''

• LEMMA-INSTANCE -- an object denoting an instance of a theorem

• LINEAR-ARITHMETIC -- A description of the linear arithmetic decision procedure

• LOCAL-INCOMPATIBILITY -- when non-local events won't replay in isolation

• LOGICAL-NAME -- a name created by a logical event

• LOOP-STOPPER -- limit application of permutative rewrite rules

• LP -- the Common Lisp entry to ACL2

• MACRO-ARGS -- the formals list of a macro definition

• MAKE-WORMHOLE-STATUS -- creates a wormhole status object from given status, entry code, and data

• MEASURE -- xargs keyword :MEASURE

• META-EXTRACT -- meta reasoning using valid terms extracted from context or world

• MODE -- xargs keyword :MODE

• NAME -- syntactic rules on logical names

• NIL-GOAL -- how to proceed when the prover generates a goal of nil

• NO-THANKS -- hints keyword :NO-THANKS

• NON-EXECUTABLE -- xargs keyword :NON-EXECUTABLE

• NON-LINEAR-ARITHMETIC -- Non-linear Arithmetic

• NONLINEARP -- hints keyword :NONLINEARP

• NORMALIZE -- xargs keyword :NORMALIZE

• NU-REWRITER -- rewriting NTH/UPDATE-NTH expressions

• OBDD -- ordered binary decision diagrams with rewriting

• ORDINALS -- ordinals in ACL2

• OTF-FLG -- allow more than one initial subgoal to be pushed for induction

• OVERRIDE-HINTS -- a list of hints given priority in every proof attempt

• P! -- to pop up (at least) one level of ACL2's command loop

• PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS -- re-defining undone defpkg s

• PARALLEL -- evaluating forms in parallel

• PARALLELISM-BUILD -- building an ACL2 executable with parallel execution enabled

• PRINT-DOC-START-COLUMN -- printing the one-liner

• PROMPT -- the prompt printed by ld

• PROOF-OF-WELL-FOUNDEDNESS -- a proof that o< is well-founded on o-p s

• PROOF-SUPPORTERS-ALIST -- See dead-events.

• REDEF -- a common way to set ld-redefinition-action

• REDEF! -- a common way to set ld-redefinition-action

• REDEF+ -- system hacker's redefinition command

• REDEF- -- turn off system hacker's redefinition command

• REDEFINED-NAMES -- to collect the names that have been redefined

• REDUNDANT-EVENTS -- allowing a name to be introduced ``twice''

• REORDER -- hints keyword :REORDER

• RESTRICT -- hints keyword :RESTRICT

• REWRITE-STACK-LIMIT -- limiting the stack depth of the ACL2 rewriter

• SAVING-AND-RESTORING -- saving and restoring your logical state

• SET-WORMHOLE-DATA -- sets the wormhole data object in a wormhole status object

• SET-WORMHOLE-ENTRY-CODE -- sets the wormhole entry code in a wormhole status object

• SHOW-BODIES -- show the potential definition bodies

• SIGNATURE -- how to specify the arity of a constrained function

• SIMPLE -- :definition and :rewrite rules used in preprocessing

• SPECIOUS-SIMPLIFICATION -- nonproductive proof steps

• SPLITTER -- reporting of rules whose application may have caused case splits

• SPLITTER-OUTPUT -- status for reporting of splitter rules

• STOBJS -- xargs keyword :STOBJS

• SUBVERSIVE-INDUCTIONS -- why we restrict encapsulated recursive functions

• SUBVERSIVE-RECURSIONS -- why we restrict encapsulated recursive functions

• SYNTAX -- the syntax of ACL2 is that of Common Lisp

• SYNTAXP -- attach a heuristic filter on a :rewrite , :meta , or :linear rule

• TERM -- the three senses of well-formed ACL2 expressions or formulas

• THE-METHOD -- how to find proofs

• TIME-TRACKER-TAU -- messages about expensive use of the tau-system

• TRUST-TAG -- See defttag.

• TTAGS-SEEN -- list some declared trust tags (ttags)

• TTREE -- tag-trees

• TYPE-SET -- how type information is encoded in ACL2

• USE -- hints keyword :USE

• USING-COMPUTED-HINTS -- how to use computed hints

• USING-COMPUTED-HINTS-1 -- Driving Home the Basics

• USING-COMPUTED-HINTS-2 -- One Hint to Every Top-Level Goal in a Forcing Round

• USING-COMPUTED-HINTS-3 -- Hints as a Function of the Goal (not its Name)

• USING-COMPUTED-HINTS-4 -- Computing the Hints

• USING-COMPUTED-HINTS-5 -- Debugging Computed Hints

• USING-COMPUTED-HINTS-6 -- Using the computed-hint-replacement feature

• USING-COMPUTED-HINTS-7 -- Using the stable-under-simplificationp flag

• USING-COMPUTED-HINTS-8 -- Some Final Comments

• USING-ENABLED-RULES -- avoiding :use hints for enabled :rewrite rules

• VERSION -- ACL2 Version Number

• WATERFALL -- See hints-and-the-waterfall.

• WHY-BRR -- an explanation of why ACL2 has an explicit brr mode

• WORLD -- ACL2 property lists and the ACL2 logical database

• WORMHOLE -- ld without state -- a short-cut to a parallel universe

• WORMHOLE-DATA -- determines the wormhole data object from a wormhole status object

• WORMHOLE-ENTRY-CODE -- determines the wormhole entry code from a wormhole status object

• WORMHOLE-EVAL -- state-saving without state -- a short-cut to a parallel universe

• WORMHOLE-IMPLEMENTATION -- notes on how wormholes are implemented

• WORMHOLE-P -- predicate to determine if you are inside a wormhole

• WORMHOLE-STATUSP -- predicate recognizing well-formed wormhole status object

• XARGS -- extra arguments, for example to give hints to defun

Perhaps as the system matures this section will become more structured.