Index
This index lists all documented topics in ACL2, arranged into sections. The first section is devoted to those whose names begin with signs (and digits), such as *STANDARD-CI* and 1+. Thereafter we have one section for each of the 26 letters of the alphabet. The last section is devoted to those topics in the ACL2-PC package. By clicking on the appropriate entry of the line below you can go to the corresponding section of the index.
You may use Find to search the Index.
We also provide an index based on Major Topics.
Signs A B C D E F G H I J K L M N O P Q R S T U V W X Y Z ACL2-PC::
&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.
* -- multiplication macro
*STANDARD-CI* -- an ACL2 character-based analogue of CLTL's *standard-input*
*STANDARD-CO* -- the ACL2 analogue of CLTL's *standard-output*
*STANDARD-OI* -- an ACL2 object-based analogue of CLTL's *standard-input*
*TERMINAL-MARKUP-TABLE* -- a markup table used for printing to the terminal
+ -- addition macro
- -- macro for subtraction and negation
/ -- macro for division and reciprocal
/= -- test inequality of two numbers
1+ -- increment by 1
1- -- decrement by 1
< -- less-than
<= -- less-than-or-equal test
= -- test equality of two numbers
> -- greater-than test
>= -- greater-than-or-equal test
@ -- get the value of a global variable in state
A Flying Tour of ACL2 -- A Flying Tour of ACL2
A Sketch of How the Rewriter Works -- A Sketch of How the Rewriter Works
A Tiny Warning Sign -- A Tiny Warning Sign
A Trivial Proof -- A Trivial Proof
A Typical State -- A Typical State
A Walking Tour of ACL2 -- A Walking Tour of ACL2
A! -- to return to the top-level of ACL2's command loop
ABORT! -- to return to the top-level of ACL2's command loop
ABOUT-ACL2 -- about ACL2
ABS -- the absolute value of a real number
ACCUMULATED-PERSISTENCE -- to get statistics on which runes are being tried
ACCUMULATED-PERSISTENCE-SUBTLETIES -- some subtle aspects of the counting done by accumulated-persistence
ACKNOWLEDGMENTS -- some contributors to the well-being of ACL2
ACL2 Characters -- ACL2 Characters
ACL2 Conses or Ordered Pairs -- ACL2 Conses or Ordered Pairs
ACL2 Strings -- ACL2 Strings
ACL2 Symbols -- ACL2 Symbols
ACL2 System Architecture -- ACL2 System Architecture
ACL2 as an Interactive Theorem Prover -- ACL2 as an Interactive Theorem Prover
ACL2 as an Interactive Theorem Prover (cont) -- ACL2 as an Interactive Theorem Prover (cont)
ACL2 is an Untyped Language -- ACL2 is an Untyped Language
ACL2-AS-STANDALONE-PROGRAM -- Calling ACL2 from another program
ACL2-BUILT-INS -- built-in ACL2 functions
ACL2-COUNT -- a commonly used measure for justifying recursion
ACL2-CUSTOMIZATION -- file of initial commands for ACL2 to run at startup
ACL2-DEFAULTS-TABLE -- a table specifying certain defaults, e.g., the default defun-mode
ACL2-HELP -- the acl2-help mailing list
ACL2-NUMBER-LISTP -- recognizer for a true list of numbers
ACL2-NUMBERP -- recognizer for numbers
ACL2-SEDAN -- ACL2 Sedan interface
ACL2-TUTORIAL -- tutorial introduction to ACL2
ACL2-USER -- a package the ACL2 user may prefer
ACL2P-KEY-CHECKPOINTS -- key checkpoints in ACL2(p)
ACL2S -- See acl2-sedan.
ACONS -- constructor for association lists
ACTIVE-RUNEP -- check that a rune exists and is enabled
ADD-BINOP -- associate a function name with a macro name
ADD-CUSTOM-KEYWORD-HINT -- add a new custom keyword hint
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
ADD-RAW-ARITY -- add arity information for raw mode
ADD-TO-SET -- add a symbol to a list
ADD-TO-SET-EQ -- See add-to-set.
ADD-TO-SET-EQL -- See add-to-set.
ADD-TO-SET-EQUAL -- See add-to-set.
ADVANCED-FEATURES -- some advanced features of ACL2
ALISTP -- recognizer for association lists
ALLOCATE-FIXNUM-RANGE -- set aside fixnums in GCL
ALPHA-CHAR-P -- recognizer for alphabetic characters
ALPHORDER -- total order on atoms
ALTERNATIVE-INTRODUCTION -- introduction to ACL2
AND -- conjunction
ANNOTATED-ACL2-SCRIPTS -- examples of ACL2 scripts
APPEND -- concatenate zero or more lists
APROPOS -- searching the documentation online
ARCHITECTURE-OF-THE-PROVER -- a simple overview of how the prover works
AREF1 -- access the elements of a 1-dimensional array
AREF2 -- access the elements of a 2-dimensional array
ARGS -- args, guard, type, constraint, etc., of a function symbol
ARRAY1P -- recognize a 1-dimensional array
ARRAY2P -- recognize a 2-dimensional array
ARRAYS -- an introduction to ACL2 arrays
ARRAYS-EXAMPLE -- an example illustrating ACL2 arrays
ASET1 -- set the elements of a 1-dimensional array
ASET2 -- set the elements of a 2-dimensional array
ASH -- arithmetic shift operation
ASSERT$ -- cause a hard error if the given test is false
ASSERT-EVENT -- assert that a given form returns a non-nil value
ASSIGN -- assign to a global variable in state
ASSOC -- look up key in association list
ASSOC-EQ -- See assoc.
ASSOC-EQUAL -- See assoc.
ASSOC-KEYWORD -- look up key in a keyword-value-listp
ASSOC-STRING-EQUAL -- look up key, a string, in association list
ATOM -- recognizer for atoms
ATOM-LISTP -- recognizer for a true list of atoms
About Models -- About Models
About Types -- About Types
About the ACL2 Home Page -- About the ACL2 Home Page
About the Admission of Recursive Definitions -- About the Admission of Recursive Definitions
About the Prompt -- About the Prompt
An Example Common Lisp Function Definition -- An Example Common Lisp Function Definition
An Example of ACL2 in Use -- An Example of ACL2 in Use
Analyzing Common Lisp Models -- Analyzing Common Lisp Models
BACKCHAIN-LIMIT -- limiting the effort expended on relieving hypotheses
BACKCHAIN-LIMIT-RW -- hints keyword :BACKCHAIN-LIMIT-RW
BACKTRACK -- hints keyword :BACKTRACK
BDD -- ordered binary decision diagrams with rewriting
BDD-ALGORITHM -- summary of the BDD algorithm in ACL2
BDD-INTRODUCTION -- examples illustrating the use of BDDs in ACL2
BIBLIOGRAPHY -- reports about ACL2
BINARY-* -- multiplication function
BINARY-+ -- addition function
BINARY-APPEND -- concatenate two lists
BIND-FREE -- to bind free variables of a rewrite or linear rule
BIND-FREE-EXAMPLES -- examples pertaining to bind-free hypotheses
BOOK-COMPILED-FILE -- creating and loading of compiled and expansion files for books
BOOK-CONTENTS -- restrictions on the forms inside books
BOOK-EXAMPLE -- how to create, certify, and use a simple book
BOOK-MAKEFILES -- makefile support provided with the ACL2 community books
BOOK-NAME -- conventions associated with book names
BOOKS -- files of ACL2 event forms
BOOLE$ -- perform a bit-wise logical operation on 2 two's complement integers
BOOLEANP -- recognizer for booleans
BOUNDERS -- intervals, bounder functions, and bounder correctness
BREAK$ -- cause an immediate Lisp break
BREAK-LEMMA -- a quick introduction to breaking rewrite rules in ACL2
BREAK-ON-ERROR -- break when encountering a hard or soft error caused by ACL2
BREAK-REWRITE -- the read-eval-print loop entered to monitor rewrite rules
BREAKS -- Common Lisp breaks
BRR -- to enable or disable the breaking of rewrite rules
BRR-COMMANDS -- Break-Rewrite Commands
BRR@ -- to access context sensitive information within break-rewrite
BUILT-IN-CLAUSE -- to build a clause into the simplifier
BUTLAST -- all but a final segment of a list
BY -- hints keyword :BY
CAAAAR -- car of the caaar
CAAADR -- car of the caadr
CAAAR -- car of the caar
CAADAR -- car of the cadar
CAADDR -- car of the caddr
CAADR -- car of the cadr
CAAR -- car of the car
CADAAR -- car of the cdaar
CADADR -- car of the cdadr
CADAR -- car of the cdar
CADDAR -- car of the cddar
CADDDR -- car of the cdddr
CADDR -- car of the cddr
CADR -- car of the cdr
CALLING-LD-IN-BAD-CONTEXTS -- errors caused by calling ld in inappropriate contexts
CANONICAL-PATHNAME -- the true absolute filename, with soft links resolved
CAR -- returns the first element of a non-empty list, else nil
CASE -- conditional based on if-then-else using eql
CASE-MATCH -- pattern matching or destructuring
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
CBD -- connected book directory string
CDAAAR -- cdr of the caaar
CDAADR -- cdr of the caadr
CDAAR -- cdr of the caar
CDADAR -- cdr of the cadar
CDADDR -- cdr of the caddr
CDADR -- cdr of the cadr
CDAR -- cdr of the car
CDDAAR -- cdr of the cdaar
CDDADR -- cdr of the cdadr
CDDAR -- cdr of the cdar
CDDDAR -- cdr of the cddar
CDDDDR -- cdr of the cdddr
CDDDR -- cdr of the cddr
CDDR -- cdr of the cdr
CDR -- returns the second element of a cons pair, else nil
CEILING -- division returning an integer by truncating toward positive infinity
CERTIFICATE -- how a book is known to be admissible and where its defpkgs reside
CERTIFY-BOOK -- how to produce a certificate for a book
CERTIFY-BOOK! -- a variant of certify-book
CHAR -- the nth element (zero-based) of a string
CHAR-CODE -- the numeric code for a given character
CHAR-DOWNCASE -- turn upper-case characters into lower-case characters
CHAR-EQUAL -- character equality without regard to case
CHAR-UPCASE -- turn lower-case characters into upper-case characters
CHAR< -- less-than test for characters
CHAR<= -- less-than-or-equal test for characters
CHAR> -- greater-than test for characters
CHAR>= -- greater-than-or-equal test for characters
CHARACTER-ALISTP -- recognizer for association lists with characters as keys
CHARACTER-ENCODING -- how bytes are parsed into characters
CHARACTER-LISTP -- recognizer for a true list of characters
CHARACTERP -- recognizer for characters
CHARACTERS -- characters in ACL2
CHECK-SUM -- assigning ``often unique'' integers to files and objects
CHECKPOINT-FORCED-GOALS -- Cause forcing goals to be checkpointed in proof trees
CLAUSE-IDENTIFIER -- the internal form of a goal-spec
CLAUSE-PROCESSOR -- make or apply a :clause-processor rule (goal-level simplifier)
CLEAR-HASH-TABLES -- deprecated feature
CLEAR-MEMOIZE-STATISTICS -- clears all profiling info displayed by (memoize-summary)
CLEAR-MEMOIZE-TABLE -- forget values remembered for the given function
CLEAR-MEMOIZE-TABLES -- forget values remembered for all the memoized functions
CLOSE-INPUT-CHANNEL -- See io.
CLOSE-OUTPUT-CHANNEL -- See io.
CLOSE-TRACE-FILE -- stop redirecting trace output to a file
CODE-CHAR -- the character corresponding to a given numeric code
COERCE -- coerce a character list to a string and a string to a list
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
COMMUNITY-BOOKS -- books contributed by the ACL2 community
COMP -- compile some ACL2 functions
COMP-GCL -- compile some ACL2 functions leaving .c and .h files
COMPILATION -- compiling ACL2 functions
COMPILING-ACL2P -- compiling ACL2(p)
COMPLEX -- create an ACL2 number
COMPLEX-RATIONALP -- recognizes complex rational numbers
COMPLEX/COMPLEX-RATIONALP -- recognizer for complex numbers
COMPOUND-RECOGNIZER -- make a rule used by the typing mechanism
COMPRESS1 -- remove irrelevant pairs from a 1-dimensional array
COMPRESS2 -- remove irrelevant pairs from a 2-dimensional array
COMPUTED-HINTS -- computing advice to the theorem proving process
CONCATENATE -- concatenate lists or strings together
COND -- conditional based on if-then-else
CONGRUENCE -- the relations to maintain while simplifying arguments
CONJUGATE -- complex number conjugate
CONS -- pair and list constructor
CONS-SUBTREES -- (cons-subtrees x nil) builds a fast alist that associates each subtree
of X with T, without duplication.
CONSERVATIVITY-OF-DEFCHOOSE -- proof of conservativity of defchoose
CONSP -- recognizer for cons pairs
CONSTRAINT -- restrictions on certain functions introduced in encapsulate events
COPYRIGHT -- ACL2 copyright, license, sponsorship
COROLLARY -- the corollary formula of a rune
COUNT -- count the number of occurrences of an item in a string or true-list
CPU-CORE-COUNT -- the number of cpu cores
CURRENT-PACKAGE -- the package used for reading and printing
CURRENT-THEORY -- currently enabled rules as of logical name
CUSTOM-KEYWORD-HINTS -- user-defined hints
CW -- print to the comment window
CW! -- print to the comment window
CW-GSTACK -- debug a rewriting loop or stack overflow
Common Lisp -- Common Lisp
Common Lisp as a Modeling Language -- Common Lisp as a Modeling Language
Conversion -- Conversion to Uppercase
Corroborating Models -- Corroborating Models
DEAD-EVENTS -- using proof supporters to identify dead code and unused theorems
DEALING-WITH-KEY-COMBINATIONS-OF-FUNCTION-SYMBOLS -- how to get rid of key combinations of function symbols
DEALING-WITH-TAU-PROBLEMS -- some advice on dealing with problems caused by the tau system
DECLARE -- declarations
DECLARE-STOBJS -- declaring a formal parameter name to be a single-threaded object
DEFABBREV -- a convenient form of macro definition for simple expansions
DEFABSSTOBJ -- define a new abstract single-threaded object
DEFABSSTOBJ-MISSING-EVENTS -- obtain the events needed to admit a defabsstobj event
DEFATTACH -- execute constrained functions using corresponding attached functions
DEFAULT -- return the :default from the header of a 1- or 2-dimensional array
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-HINTS-TABLE -- a table used to provide hints for proofs
DEFAULT-PRINT-PROMPT -- the default prompt printed by ld
DEFAULT-RULER-EXTENDERS -- the default ruler-extenders for defun'd functions
DEFAULT-TOTAL-PARALLELISM-WORK-LIMIT -- for ACL2(p): returns the default value for global total-parallelism-work-limit
DEFAULT-VERIFY-GUARDS-EAGERNESS -- See set-verify-guards-eagerness.
DEFAXIOM -- add an axiom
DEFCHOOSE -- define a Skolem (witnessing) function
DEFCONG -- prove congruence rule
DEFCONST -- define a constant
DEFDOC -- add a documentation topic
DEFEQUIV -- prove that a function is an equivalence relation
DEFEVALUATOR -- introduce an evaluator function
DEFEXEC -- attach a terminating executable function to a definition
DEFINE-PC-HELP -- define a macro command whose purpose is to print something
DEFINE-PC-MACRO -- define a proof-checker macro command
DEFINE-PC-META -- define a proof-checker meta command
DEFINE-TRUSTED-CLAUSE-PROCESSOR -- define a trusted (unverified) goal-level simplifier
DEFINITION -- make a rule that acts like a function definition
DEFLABEL -- build a landmark and/or add a documentation topic
DEFLOCK -- define a wrapper macro that provides mutual exclusion in ACL2(p)
DEFMACRO -- define a macro
DEFMACRO-LAST -- define a macro that returns its last argument, but with side effects
DEFN -- definition with guard t
DEFND -- disabled definition with guard t
DEFPKG -- define a new symbol package
DEFPROXY -- define a non-executable :program-mode function for attachment
DEFPUN -- define a tail-recursive function symbol
DEFREFINEMENT -- prove that equiv1 refines equiv2
DEFSTOBJ -- define a new single-threaded object
DEFSTUB -- stub-out a function symbol
DEFTHEORY -- define a theory (to enable or disable a set of rules)
DEFTHEORY-STATIC -- define a `static' theory (to enable or disable a set of rules)
DEFTHM -- prove and name a theorem
DEFTHMD -- prove and name a theorem and then disable it
DEFTTAG -- introduce a trust tag (ttag)
DEFUN -- define a function symbol
DEFUN-INLINE -- define a potentially inlined function symbol and associated macro
DEFUN-MODE -- determines whether a function definition is a logical act
DEFUN-MODE-CAVEAT -- potential soundness issue for functions with defun-mode :program
DEFUN-NOTINLINE -- define a not-to-be-inlined function symbol and associated macro
DEFUN-NX -- define a non-executable function symbol
DEFUN-SK -- define a function whose body has an outermost quantifier
DEFUN-SK-EXAMPLE -- a simple example using defun-sk
DEFUND -- define a function symbol and then disable it
DEFUND-INLINE -- define a potentially disabled, inlined function symbol and associated macro
DEFUND-NOTINLINE -- define a disabled, not-to-be-inlined function symbol and associated macro
DEFUNS -- an alternative to mutual-recursion
DELETE-ASSOC -- modify an association list by associating a value with a key
DELETE-ASSOC-EQ -- See delete-assoc.
DELETE-ASSOC-EQUAL -- See delete-assoc.
DELETE-INCLUDE-BOOK-DIR -- unlink keyword for :dir argument of ld and include-book
DENOMINATOR -- divisor of a ratio in lowest terms
DIGIT-CHAR-P -- the number, if any, corresponding to a given character
DIGIT-TO-CHAR -- map a digit to a character
DIMENSIONS -- return the :dimensions from the header of a 1- or 2-dimensional array
DISABLE -- deletes names from current theory
DISABLE-FORCING -- to disallow forced case-splits
DISABLE-IMMEDIATE-FORCE-MODEP -- forced hypotheses are not attacked immediately
DISABLEDP -- determine whether a given name or rune is disabled
DISASSEMBLE$ -- disassemble a function
DIVE-INTO-MACROS-TABLE -- right-associated function information for the proof-checker
DMR -- dynamically monitor rewrites and other prover activity
DO-NOT -- hints keyword :DO-NOT
DO-NOT-INDUCT -- hints keyword :DO-NOT-INDUCT
DOC -- brief documentation (type :doc name)
DOC! -- all the documentation for a name (type :doc! name)
DOC-STRING -- formatted documentation strings
DOCS -- available documentation topics (by section)
DOCUMENTATION -- functions that display documentation
DOUBLE-REWRITE -- cause a term to be rewritten twice
DYNAMICALLY-MONITOR-REWRITES -- See dmr.
E/D -- enable/disable rules
E0-ORD-< -- the old ordering function for ACL2 ordinals
E0-ORDINALP -- the old recognizer for ACL2 ordinals
EARLY-TERMINATION -- early termination for pand and por.
EC-CALL -- execute a call in the ACL2 logic instead of raw Lisp
EIGHTH -- eighth member of the list
ELIM -- make a destructor elimination rule
EMACS -- emacs support for ACL2
EMBEDDED-EVENT-FORM -- forms that may be embedded in other events
ENABLE -- adds names to current theory
ENABLE-FORCING -- to allow forced splits
ENABLE-IMMEDIATE-FORCE-MODEP -- forced hypotheses are attacked immediately
ENCAPSULATE -- constrain some functions and/or hide some events
ENDP -- recognizer for empty lists
ENTER-BOOT-STRAP-MODE -- The first millisecond of the Big Bang
EQ -- equality of symbols
EQL -- test equality (of two numbers, symbols, or characters)
EQLABLE-ALISTP -- recognizer for a true list of pairs whose cars are suitable for eql
EQLABLE-LISTP -- recognizer for a true list of objects each suitable for eql
EQLABLEP -- the guard for the function eql
EQUAL -- true equality
EQUALITY-VARIANTS -- versions of a function using different equality tests
EQUALITY-VARIANTS-DETAILS -- details about equality-variants
EQUIVALENCE -- mark a relation as an equivalence relation
EQUIVALENT-FORMULAS-DIFFERENT-REWRITE-RULES -- logically equivalent formulas can generate radically different rules
ER -- print an error message and ``cause an error''
ER-PROGN -- perform a sequence of state-changing ``error triples''
ERROR-TRIPLES -- a common ACL2 programming idiom
ERROR-TRIPLES-AND-PARALLELISM -- how to avoid error triples in ACL2(p)
ERROR1 -- print an error message and cause a ``soft error''
ESCAPE-TO-COMMON-LISP -- escaping to Common Lisp
EVALUATOR-RESTRICTIONS -- some restrictions on the use of evaluators in meta-level rules
EVENP -- test whether an integer is even
EVENTS -- functions that extend the logic
EVISC-TABLE -- support for abbreviated output
EVISC-TUPLE -- control suppression of details when printing
EVISCERATE-HIDE-TERMS -- to print (hide ...) as <hidden>
EXAMPLE-INDUCTION-SCHEME-BINARY-TREES -- induction on binary trees
EXAMPLE-INDUCTION-SCHEME-DOWN-BY-2 -- induction downwards 2 steps at a time
EXAMPLE-INDUCTION-SCHEME-NAT-RECURSION -- induction on natural numbers
EXAMPLE-INDUCTION-SCHEME-ON-LISTS -- induction on lists
EXAMPLE-INDUCTION-SCHEME-ON-SEVERAL-VARIABLES -- induction on several variables
EXAMPLE-INDUCTION-SCHEME-UPWARDS -- induction upwards
EXAMPLE-INDUCTION-SCHEME-WITH-ACCUMULATORS -- induction scheme with accumulators
EXAMPLE-INDUCTION-SCHEME-WITH-MULTIPLE-INDUCTION-STEPS -- induction scheme with more than one induction step
EXAMPLE-INDUCTIONS -- some examples of induction schemes in ACL2
EXECUTABLE-COUNTERPART -- a rule for computing the value of a function
EXECUTABLE-COUNTERPART-THEORY -- executable counterpart rules as of logical name
EXISTS -- existential quantifier
EXIT -- quit entirely out of Lisp
EXIT-BOOT-STRAP-MODE -- the end of pre-history
EXPAND -- hints keyword :EXPAND
EXPLODE-NONNEGATIVE-INTEGER -- the list of characters in the radix-r form of a number
EXPT -- exponential function
EXTENDED-METAFUNCTIONS -- state and context sensitive metafunctions
EXTERNAL-FORMAT -- See character-encoding.
EXTRA-INFO -- generate markers to indicate sources of guard proof obligations
Evaluating App on Sample Input -- Evaluating App on Sample Input
F-GET-GLOBAL -- get the value of a global variable in state
F-PUT-GLOBAL -- assign to a global variable in state
FAILED-FORCING -- how to deal with a proof failure in a forcing round
FAILURE -- how to deal with a proof failure
FAST-ALIST-FREE -- (fast-alist-free alist) throws away the hash table associated with a fast
alist.
FAST-ALIST-FREE-ON-EXIT -- Free a fast alist after the completion of some form.
FAST-ALIST-LEN -- (fast-alist-len alist) counts the number of unique keys in a fast alist.
FAST-ALIST-SUMMARY -- (fast-alist-summary) prints some basic statistics about any current fast
alists.
FAST-ALISTS -- alists with hidden hash tables for faster execution
FC-REPORT -- to report on the forward chaining activity in the most recent proof
FIFTH -- fifth member of the list
FILE-READING-EXAMPLE -- example of reading files in ACL2
FINALIZE-EVENT-USER -- user-supplied code to complete events, e.g., with extra summary output
FIND-RULES-OF-RUNE -- find the rules named rune
FIRST -- first member of the list
FIX -- coerce to a number
FIX-TRUE-LIST -- coerce to a true list
FLET -- local binding of function symbols
FLOOR -- division returning an integer by truncating toward negative infinity
FLUSH-COMPRESS -- flush the under-the-hood array for the given name
FLUSH-HONS-GET-HASH-TABLE-LINK -- deprecated feature
FMS -- :(str alist co-channel state evisc) => state
FMS! -- :(str alist co-channel state evisc) => state
FMS!-TO-STRING -- See printing-to-strings.
FMS-TO-STRING -- See printing-to-strings.
FMT -- formatted printing
FMT! -- :(str alist co-channel state evisc) => state
FMT!-TO-STRING -- See printing-to-strings.
FMT-TO-COMMENT-WINDOW -- print to the comment window
FMT-TO-STRING -- See printing-to-strings.
FMT1 -- :(str alist col co-channel state evisc) => (mv col state)
FMT1! -- :(str alist col channel state evisc) => (mv col state)
FMT1!-TO-STRING -- See printing-to-strings.
FMT1-TO-STRING -- See printing-to-strings.
FORALL -- universal quantifier
FORCE -- identity function used to force a hypothesis
FORCED -- See force.
FORCING-ROUND -- a section of a proof dealing with forced assumptions
FORWARD-CHAINING -- make a rule to forward chain when a certain trigger arises
FORWARD-CHAINING-REPORTS -- to see reports about the forward chaining process
FOURTH -- fourth member of the list
FREE-VARIABLES -- free variables in rules
FREE-VARIABLES-EXAMPLES -- examples pertaining to free variables in rules
FREE-VARIABLES-EXAMPLES-FORWARD-CHAINING -- examples pertaining to free variables in forward-chaining rules
FREE-VARIABLES-EXAMPLES-REWRITE -- examples pertaining to free variables in rewrite rules
FREE-VARIABLES-TYPE-PRESCRIPTION -- matching for free variable in type-prescription rules
FREQUENTLY-ASKED-QUESTIONS-BY-NEWCOMERS -- some questions newcomers frequently ask
FULL-BOOK-NAME -- book naming conventions assumed by ACL2
FUNCTION-THEORY -- function symbol rules as of logical name
FUNCTIONAL-INSTANTIATION-EXAMPLE -- a small proof demonstrating functional instantiation
FUNCTIONAL-INSTANTIATION-IN-ACL2R -- additional requirements for :functional-instance hints in ACL2(r)
FURTHER-INFORMATION-ON-REWRITING -- a grab bag of advice and information on rewriting
FUTURE-WORK-RELATED-TO-THE-TAU-SYSTEM -- some tau system problems that we hope someone will address
Flawed Induction Candidates in App Example -- Flawed Induction Candidates in App Example
Free Variables in Top-Level Input -- Free Variables in Top-Level Input
Functions for Manipulating these Objects -- Functions for Manipulating these Objects
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
GCS -- See get-command-sequence.
GENERALIZE -- make a rule to restrict generalizations
GENERALIZED-BOOLEANS -- potential soundness issues related to ACL2 predicates
GENERALIZING-KEY-CHECKPOINTS -- getting rid of unnecessary specificity
GET-COMMAND-SEQUENCE -- return list of commands that are between two command descriptors
GET-OUTPUT-STREAM-STRING$ -- See io.
GET-WORMHOLE-STATUS -- make a wormhole's status visible outside the wormhole
GETENV$ -- read an environment variable
GETPROP -- access fast property lists
GOAL-SPEC -- to indicate where a hint is to be used
GOOD-ATOM-LISTP -- recognizer for a true list of ``good'' atoms
GOOD-BYE -- quit entirely out of Lisp
GRANULARITY -- limit the amount of parallelism
GROUND-ZERO -- enabled rules in the startup theory
GUARD -- restricting the domain of a function
GUARD-DEBUG -- generate markers to indicate sources of guard proof obligations
GUARD-EVALUATION-EXAMPLES-LOG -- log showing combinations of defun-modes and guard-checking
GUARD-EVALUATION-EXAMPLES-SCRIPT -- a script to show combinations of defun-modes and guard-checking
GUARD-EVALUATION-TABLE -- a table that shows combinations of defun-modes and guard-checking
GUARD-EXAMPLE -- a brief transcript illustrating guards in ACL2
GUARD-HINTS -- xargs keyword :GUARD-HINTS
GUARD-INTRODUCTION -- introduction to guards in ACL2
GUARD-MISCELLANY -- miscellaneous remarks about guards
GUARD-OBLIGATION -- the guard proof obligation
GUARD-QUICK-REFERENCE -- brief summary of guard checking and guard verification
GUARDS-AND-EVALUATION -- the relationship between guards and evaluation
GUARDS-FOR-SPECIFICATION -- guards as a specification device
Guards -- Guards
Guessing the Type of a Newly Admitted Function -- Guessing the Type of a Newly Admitted Function
Guiding the ACL2 Theorem Prover -- Guiding the ACL2 Theorem Prover
HANDS-OFF -- hints keyword :HANDS-OFF
HARD-ERROR -- print an error message and stop execution
HEADER -- return the header of a 1- or 2-dimensional array
HELP -- brief survey of ACL2 features
HIDDEN-DEATH-PACKAGE -- handling defpkg events that are local
HIDDEN-DEFPKG -- handling defpkg events that are local
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
HISTORY -- functions that display or change history
HONS -- (hons x y) returns a normed object equal to (cons x y).
HONS-ACONS -- (hons-acons key val alist) is the main way to create or extend
fast-alists.
HONS-ACONS! -- (hons-acons! key val alist) is an alternative to hons-acons that
produces normed, fast alists.
HONS-AND-MEMOIZATION -- hash cons, function memoization, and applicative hash tables
HONS-ASSOC-EQUAL -- (hons-assoc-equal key alist) is not fast; it serves as the logical
definition for hons-get.
HONS-CLEAR -- (hons-clear gc) is a drastic garbage collection mechanism that clears out
the underlying Hons Space.
HONS-COPY -- (hons-copy x) returns a normed object that is equal to X.
HONS-COPY-PERSISTENT -- (hons-copy-persistent x) returns a normed object that is equal to X
and which will be re-normed after any calls to hons-clear.
HONS-EQUAL -- (hons-equal x y) is a recursive equality check that optimizes when parts of
its arguments are normed.
HONS-EQUAL-LITE -- (hons-equal-lite x y) is a non-recursive equality check that optimizes if
its arguments are normed.
HONS-GET -- (hons-get key alist) is the efficient lookup operation for
fast-alists.
HONS-NOTE -- notes about HONS, especially pertaining to expensive resizing operations
HONS-RESIZE -- (hons-resize ...) can be used to manually adjust the sizes of the hash
tables that govern which ACL2 Objects are considered normed.
HONS-SHRINK-ALIST -- (hons-shrink-alist alist ans) can be used to eliminate "shadowed pairs"
from an alist or to copy fast-alists.
HONS-SHRINK-ALIST! -- (hons-shrink-alist! alist ans) is an alternative to hons-shrink-alist
that produces a normed result.
HONS-SUMMARY -- (hons-summary) prints basic information about the sizes of the tables in
the current Hons Space.
HONS-WASH -- (hons-wash) is like gc$ but can also garbage collect normed
objects (CCL Only).
Hey Wait! Is ACL2 Typed or Untyped(Q) -- Hey Wait! Is ACL2 Typed or Untyped?
How Long Does It Take to Become an Effective User(Q) -- How Long Does It Take to Become an Effective User?
How To Find Out about ACL2 Functions -- How To Find Out about ACL2 Functions
How To Find Out about ACL2 Functions (cont) -- How To Find Out about ACL2 Functions (cont)
I-AM-HERE -- a convenient marker for use with rebuild
I-CLOSE -- ACL2(r) test for whether two numbers are infinitesimally close
I-LARGE -- ACL2(r) recognizer for infinitely large numbers
I-LIMITED -- ACL2(r) recognizer for limited numbers
I-SMALL -- ACL2(r) recognizer for infinitesimal numbers
IDENTITY -- the identity function
IF -- if-then-else function
IF* -- for conditional rewriting with BDDs
IF-INTRO -- See splitter.
IFF -- logical ``if and only if''
IFIX -- coerce to an integer
IGNORABLE -- See declare.
IGNORE -- See declare.
ILLEGAL -- print an error message and stop execution
IMAGPART -- imaginary part of a complex number
IMMED-FORCED -- See splitter.
IMMEDIATE-FORCE-MODEP -- when executable counterpart is enabled,
forced hypotheses are attacked immediately
IMPLIES -- logical implication
IMPROPER-CONSP -- recognizer for improper (non-null-terminated) non-empty lists
IN-ARITHMETIC-THEORY -- designate theory for some rewriting done for non-linear arithmetic
IN-PACKAGE -- select current package
IN-TAU-INTERVALP -- Boolean membership in a tau interval
IN-THEORY -- designate ``current'' theory (enabling its rules)
INCLUDE-BOOK -- load the events in a file
INCOMPATIBLE -- declaring that two rules should not both be enabled
INDUCT -- hints keyword :INDUCT
INDUCTION -- make a rule that suggests a certain induction
INITIALIZE-EVENT-USER -- user-supplied code to initiate events
INSTRUCTIONS -- instructions to the proof checker
INT= -- test equality of two integers
INTEGER-LENGTH -- number of bits in two's complement integer representation
INTEGER-LISTP -- recognizer for a true list of integers
INTEGERP -- recognizer for whole numbers
INTERESTING-APPLICATIONS -- some industrial examples of ACL2 use
INTERN -- create a new symbol in a given package
INTERN$ -- create a new symbol in a given package
INTERN-IN-PACKAGE-OF-SYMBOL -- create a symbol with a given name
INTERSECTION$ -- elements of one list that are not elements of another
INTERSECTION-EQ -- See intersection$.
INTERSECTION-EQUAL -- See intersection$.
INTERSECTION-THEORIES -- intersect two theories
INTERSECTP -- test whether two lists intersect
INTERSECTP-EQ -- See intersectp.
INTERSECTP-EQUAL -- See intersectp.
INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS -- the mechanics of interaction with the theorem prover
INTRODUCTION-TO-HINTS -- how to provide hints to the theorem prover
INTRODUCTION-TO-KEY-CHECKPOINTS -- What questions to ask at key checkpoints
INTRODUCTION-TO-REWRITE-RULES-PART-1 -- introduction to ACL2's notion of rewrite rules
INTRODUCTION-TO-REWRITE-RULES-PART-2 -- how to arrange rewrite rules
INTRODUCTION-TO-THE-DATABASE -- how to update the database
INTRODUCTION-TO-THE-TAU-SYSTEM -- a decision procedure for runtime types
INTRODUCTION-TO-THE-THEOREM-PROVER -- how the theorem prover works -- level 0
INTRODUCTORY-CHALLENGE-PROBLEM-1 -- challenge problem 1 for the new user of ACL2
INTRODUCTORY-CHALLENGE-PROBLEM-1-ANSWER -- answer to challenge problem 1 for the new user of ACL2
INTRODUCTORY-CHALLENGE-PROBLEM-2 -- challenge problem 2 for the new user of ACL2
INTRODUCTORY-CHALLENGE-PROBLEM-2-ANSWER -- answer to challenge problem 2 for the new user of ACL2
INTRODUCTORY-CHALLENGE-PROBLEM-3 -- challenge problem 3 for the new user of ACL2
INTRODUCTORY-CHALLENGE-PROBLEM-3-ANSWER -- answer to challenge problem 3 for the new user of ACL2
INTRODUCTORY-CHALLENGE-PROBLEM-4 -- challenge problem 4 for the new user of ACL2
INTRODUCTORY-CHALLENGE-PROBLEM-4-ANSWER -- answer to challenge problem 4 for the new user of ACL2
INTRODUCTORY-CHALLENGES -- challenge problems for the new ACL2 user
INVISIBLE-FNS-TABLE -- functions that are invisible to the loop-stopper algorithm
IO -- input/output facilities in ACL2
IPRINT -- See set-iprint.
IPRINTING -- See set-iprint.
IRRELEVANT-FORMALS -- formals that are used but only insignificantly
J
KEEP -- how we know if include-book read the correct files
KEYWORD -- See keywordp.
KEYWORD-COMMANDS -- how keyword commands are processed
KEYWORD-VALUE-LISTP -- recognizer for true lists whose even-position elements are keywords
KEYWORDP -- recognizer for keywords
KWOTE -- quote an arbitrary object
KWOTE-LST -- quote an arbitrary true list of objects
LAMBDA -- See term.
LAST -- the last cons (not element) of a list
LD -- the ACL2 read-eval-print loop, file loader, and command processor
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
LEN -- length of a list
LENGTH -- length of a string or proper list
LET -- binding of lexically scoped (local) variables
LET* -- binding of lexically scoped (local) variables
LEXORDER -- total order on ACL2 objects
LINEAR -- make some arithmetic inequality rules
LINEAR-ARITHMETIC -- A description of the linear arithmetic decision procedure
LIST -- build a list
LIST* -- build a list
LISTP -- recognizer for (not necessarily proper) lists
LOCAL -- hiding an event in an encapsulation or book
LOCAL-INCOMPATIBILITY -- when non-local events won't replay in isolation
LOGAND -- bitwise logical `and' of zero or more integers
LOGANDC1 -- bitwise logical `and' of two ints, complementing the first
LOGANDC2 -- bitwise logical `and' of two ints, complementing the second
LOGBITP -- the ith bit of an integer
LOGCOUNT -- number of ``on'' bits in a two's complement number
LOGEQV -- bitwise logical equivalence of zero or more integers
LOGIC -- to set the default defun-mode to :logic
LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED -- background knowledge in ACL2 logic for theorem prover tutorial
LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-BASE-CASE -- a brief explanation of base cases
LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-EQUALS-FOR-EQUALS -- substitution of equals for equals
LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-EVALUATION -- evaluation during proofs
LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF -- a brief explanation of induction
LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INSTANCE -- a brief explanation of substitution instances
LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-PROPOSITIONAL-CALCULUS -- a brief explanation of propositional calculus
LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-Q1-ANSWER -- the inductive step of the rev-rev proof -- Answer to Question 1
LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-Q2-ANSWER -- the inductive step of the rev-rev proof -- Answer to Question 2
LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-Q3-ANSWER -- the inductive step of the rev-rev proof -- Answer to Question 2
LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-REWRITING -- a brief explanation of rewriting from the logical perspective
LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-REWRITING-REPEATEDLY -- further information on expanding definitions via rewriting
LOGICAL-NAME -- a name created by a logical event
LOGIOR -- bitwise logical inclusive or of zero or more integers
LOGNAND -- bitwise logical `nand' of two integers
LOGNOR -- bitwise logical `nor' of two integers
LOGNOT -- bitwise not of a two's complement number
LOGORC1 -- bitwise logical inclusive or of two ints, complementing the first
LOGORC2 -- bitwise logical inclusive or of two ints, complementing the second
LOGTEST -- test if two integers share a `1' bit
LOGXOR -- bitwise logical exclusive or of zero or more integers
LOOP-STOPPER -- limit application of permutative rewrite rules
LOWER-CASE-P -- recognizer for lower case characters
LP -- the Common Lisp entry to ACL2
MACRO-ALIASES-TABLE -- a table used to associate function names with macro names
MACRO-ARGS -- the formals list of a macro definition
MACRO-COMMAND -- compound command for the proof-checker
MAKE-CHARACTER-LIST -- coerce to a list of characters
MAKE-EVENT -- evaluate (expand) a given form and then evaluate the result
MAKE-EVENT-DETAILS -- details on make-event expansion
MAKE-FAST-ALIST -- (make-fast-alist alist) creates a fast-alist from the input alist,
returning alist itself or, in some cases, a new object equal to it.
MAKE-LIST -- make a list of a given size
MAKE-ORD -- a constructor for ordinals.
MAKE-TAU-INTERVAL -- make a tau interval
MAKE-WORMHOLE-STATUS -- creates a wormhole status object from given status, entry code, and data
MAKEFILES -- See book-makefiles.
MANAGING-ACL2-PACKAGES -- user-contributed documentation on packages
MARKUP -- the markup language for ACL2 documentation strings
MAX -- the larger of two numbers
MAXIMUM-LENGTH -- return the :maximum-length from the header of an array
MBE -- attach code for execution
MBE1 -- attach code for execution
MBT -- introduce a test not to be evaluated
MEASURE -- xargs keyword :MEASURE
MEMBER -- membership predicate
MEMBER-EQ -- See member.
MEMBER-EQUAL -- See member.
MEMOIZE -- turn on memoization for a specified function
MEMOIZE-SUMMARY -- display all collected profiling and memoization table info
MEMSUM -- display all collected profiling and memoization info
META -- make a :meta rule (a hand-written simplifier)
META-EXTRACT -- meta reasoning using valid terms extracted from context or world
MIN -- the smaller of two numbers
MINIMAL-THEORY -- a minimal theory to enable
MINUSP -- test whether a number is negative
MISCELLANEOUS -- a miscellany of documented functions and concepts
(often cited in more accessible documentation)
MOD -- remainder using floor
MOD-EXPT -- exponential function
MODE -- xargs keyword :MODE
MONITOR -- to monitor the attempted application of a rule name
MONITORED-RUNES -- print the monitored runes and their break conditions
MORE -- your response to :doc or :more's ``(type :more...)''
MORE! -- another response to ``(type :more for more, :more! for the rest)''
MORE-DOC -- a continuation of the :doc documentation
MUST-BE-EQUAL -- attach code for execution
MUTUAL-RECURSION -- define some mutually recursive functions
MUTUAL-RECURSION-PROOF-EXAMPLE -- a small proof about mutually recursive functions
MV -- returning a multiple value
MV-LET -- calling multi-valued ACL2 functions
MV-LIST -- converting multiple-valued result to a single-valued list
MV-NTH -- the mv-nth element (zero-based) of a list
MV? -- return one or more values
MV?-LET -- calling possibly multi-valued ACL2 functions
Modeling in ACL2 -- Modeling in ACL2
Models in Engineering -- Models in Engineering
Models of Computer Hardware and Software -- Models of Computer Hardware and Software
NAME -- syntactic rules on logical names
NAT-LISTP -- recognizer for a true list of natural numbers
NATP -- a recognizer for the natural numbers
NFIX -- coerce to a natural number
NIL-GOAL -- how to proceed when the prover generates a goal of nil
NINTH -- ninth member of the list
NO-DUPLICATESP -- check for duplicates in a list
NO-DUPLICATESP-EQ -- See no-duplicatesp.
NO-DUPLICATESP-EQUAL -- See no-duplicatesp.
NO-THANKS -- hints keyword :NO-THANKS
NON-EXEC -- mark code as non-executable
NON-EXECUTABLE -- xargs keyword :NON-EXECUTABLE
NON-LINEAR-ARITHMETIC -- Non-linear Arithmetic
NONLINEARP -- hints keyword :NONLINEARP
NONNEGATIVE-INTEGER-QUOTIENT -- natural number division function
NORMALIZE -- xargs keyword :NORMALIZE
NORMED -- Normed objects are ACL2 Objects that are "canonical" or "unique" in a
certain sense.
NOT -- logical negation
NOTE-2-0 -- ACL2 Version 2.0 (July, 1997) Notes
NOTE-2-1 -- ACL2 Version 2.1 (December, 1997) Notes
NOTE-2-2 -- ACL2 Version 2.2 (August, 1998) Notes
NOTE-2-3 -- ACL2 Version 2.3 (October, 1998) Notes
NOTE-2-4 -- ACL2 Version 2.4 (August, 1999) Notes
NOTE-2-5 -- ACL2 Version 2.5 (June, 2000) Notes
NOTE-2-5(R) -- ACL2 Version 2.5(r) (June, 2000) Notes
NOTE-2-6 -- ACL2 Version 2.6 (November, 2001) Notes
NOTE-2-6(R) -- ACL2 Version 2.6(r) (November, 2001) Notes
NOTE-2-6-GUARDS -- ACL2 Version 2.6 Notes on Guard-related Changes
NOTE-2-6-NEW-FUNCTIONALITY -- ACL2 Version 2.6 Notes on New Functionality
NOTE-2-6-OTHER -- ACL2 Version 2.6 Notes on Other (Minor) Changes
NOTE-2-6-PROOF-CHECKER -- ACL2 Version 2.6 Notes on Proof-checker Changes
NOTE-2-6-PROOFS -- ACL2 Version 2.6 Notes on Changes in Proof Engine
NOTE-2-6-RULES -- ACL2 Version 2.6 Notes on Changes in Rules and Constants
NOTE-2-6-SYSTEM -- ACL2 Version 2.6 Notes on System-level Changes
NOTE-2-7 -- ACL2 Version 2.7 (November, 2002) Notes
NOTE-2-7(R) -- ACL2 Version 2.7(r) (November, 2002) Notes
NOTE-2-7-BUG-FIXES -- ACL2 Version 2.7 Notes on Bug Fixes
NOTE-2-7-GUARDS -- ACL2 Version 2.7 Notes on Guard-related Changes
NOTE-2-7-NEW-FUNCTIONALITY -- ACL2 Version 2.7 Notes on New Functionality
NOTE-2-7-OTHER -- ACL2 Version 2.7 Notes on Miscellaneous Changes
NOTE-2-7-PROOF-CHECKER -- ACL2 Version 2.7 Notes on Proof-checker Changes
NOTE-2-7-PROOFS -- ACL2 Version 2.7 Notes on Changes in Proof Engine
NOTE-2-7-RULES -- ACL2 Version 2.7 Notes on Changes in Rules and Constants
NOTE-2-7-SYSTEM -- ACL2 Version 2.7 Notes on System-level Changes
NOTE-2-8 -- ACL2 Version 2.8 (March, 2004) Notes
NOTE-2-8(R) -- ACL2 Version 2.8(r) (March, 2003) Notes
NOTE-2-8-BUG-FIXES -- ACL2 Version 2.8 Notes on Bug Fixes
NOTE-2-8-GUARDS -- ACL2 Version 2.8 Notes on Guard-related Changes
NOTE-2-8-NEW-FUNCTIONALITY -- ACL2 Version 2.8 Notes on New Functionality
NOTE-2-8-ORDINALS -- ACL2 Version 2.8 Notes on Changes to the Ordinals
NOTE-2-8-OTHER -- ACL2 Version 2.8 Notes on Miscellaneous Changes
NOTE-2-8-PROOF-CHECKER -- ACL2 Version 2.8 Notes on Proof-checker Changes
NOTE-2-8-PROOFS -- ACL2 Version 2.8 Notes on Changes in Proof Engine
NOTE-2-8-RULES -- ACL2 Version 2.8 Notes on Changes in Rules, Definitions, and Constants
NOTE-2-8-SYSTEM -- ACL2 Version 2.8 Notes on System-level Changes
NOTE-2-9 -- ACL2 Version 2.9 (October, 2004) Notes
NOTE-2-9(R) -- ACL2 Version 2.9(r) (October, 2004) Notes
NOTE-2-9-1 -- ACL2 Version 2.9.1 (December, 2004) Notes
NOTE-2-9-2 -- ACL2 Version 2.9.2 (April, 2005) Notes
NOTE-2-9-3 -- ACL2 Version 2.9.3 (August, 2005) Notes
NOTE-2-9-3-PPR-CHANGE -- change in pretty-printing for ACL2 Version_2.9.3
NOTE-2-9-4 -- ACL2 Version 2.9.4 (February, 2006) Notes
NOTE-2-9-5 -- Changes in Version 3.0 since Version 2.9.4
NOTE-3-0 -- ACL2 Version 3.0 (June, 2006) Notes
NOTE-3-0(R) -- ACL2 Version 3.0(r) (June, 2006) Notes
NOTE-3-0-1 -- ACL2 Version 3.0.1 (August, 2006) Notes
NOTE-3-0-1(R) -- ACL2 Version 3.0.1(r) (August, 2006) Notes
NOTE-3-0-2 -- ACL2 Version 3.0.2 (December, 2006) Notes
NOTE-3-1 -- ACL2 Version 3.1 (December, 2006) Notes
NOTE-3-1(R) -- ACL2 Version 3.1(r) (December, 2006) Notes
NOTE-3-2 -- ACL2 Version 3.2 (April, 2007) Notes
NOTE-3-2(R) -- ACL2 Version 3.2(r) (April, 2007) Notes
NOTE-3-2-1 -- ACL2 Version 3.2.1 (June, 2007) Notes
NOTE-3-2-1(R) -- ACL2 Version 3.2.1(r) (June, 2007) Notes
NOTE-3-3 -- ACL2 Version 3.3 (November, 2007) Notes
NOTE-3-3(R) -- ACL2 Version 3.3(r) (November, 2007) Notes
NOTE-3-4 -- ACL2 Version 3.4 (August, 2008) Notes
NOTE-3-4(R) -- ACL2 Version 3.4(r) (August, 2008) Notes
NOTE-3-5 -- ACL2 Version 3.5 (May, 2009) Notes
NOTE-3-5(R) -- ACL2 Version 3.5(r) (May, 2009) Notes
NOTE-3-6 -- ACL2 Version 3.6 (August, 2009) Notes
NOTE-3-6(R) -- ACL2 Version 3.6(r) (August, 2009) Notes
NOTE-3-6-1 -- ACL2 Version 3.6.1 (September, 2009) Notes
NOTE-4-0 -- ACL2 Version 4.0 (July, 2010) Notes
NOTE-4-0(R) -- ACL2 Version 4.0(r) (July, 2010) Notes
NOTE-4-0-WORMHOLE-CHANGES -- how to convert calls of wormhole for Version 4.0
NOTE-4-1 -- ACL2 Version 4.1 (September, 2010) Notes
NOTE-4-1(R) -- ACL2 Version 4.1(r) (September, 2010) Notes
NOTE-4-2 -- ACL2 Version 4.2 (January, 2011) Notes
NOTE-4-2(R) -- ACL2 Version 4.2(r) (January, 2011) Notes
NOTE-4-3 -- ACL2 Version 4.3 (July, 2011) Notes
NOTE-4-3(R) -- ACL2 Version 4.3(r) (July, 2011) Notes
NOTE-5-0 -- ACL2 Version 5.0 (August, 2012) Notes
NOTE-6-0 -- ACL2 Version 6.0 (December, 2012) Notes
NOTE-6-1 -- ACL2 Version 6.1 (February, 2013) Notes
NOTE1 -- Acl2 Version 1.1 Notes
NOTE2 -- Acl2 Version 1.2 Notes
NOTE3 -- Acl2 Version 1.3 Notes
NOTE4 -- Acl2 Version 1.4 Notes
NOTE5 -- Acl2 Version 1.5 Notes
NOTE6 -- Acl2 Version 1.6 Notes
NOTE7 -- ACL2 Version 1.7 (released October 1994) Notes
NOTE8 -- ACL2 Version 1.8 (May, 1995) Notes
NOTE8-UPDATE -- ACL2 Version 1.8 (Summer, 1995) Notes
NOTE9 -- ACL2 Version 1.9 (Fall, 1996) Notes
NQTHM-TO-ACL2 -- ACL2 analogues of Nqthm functions and commands
NTH -- the nth element (zero-based) of a list
NTH-ALIASES-TABLE -- a table used to associate names for nth/update-nth printing
NTHCDR -- final segment of a list
NU-REWRITER -- rewriting NTH/UPDATE-NTH expressions
NULL -- recognizer for the empty list
NUMBER-SUBTREES -- (number-subtrees x) returns the number of distinct subtrees of X, in the
sense of equal
NUMERATOR -- dividend of a ratio in lowest terms
Name the Formula Above -- Name the Formula Above
Nontautological Subgoals -- Prover output omits some details
Numbers in ACL2 -- Numbers in ACL2
O-FINP -- recognizes if an ordinal is finite
O-FIRST-COEFF -- returns the first coefficient of an ordinal
O-FIRST-EXPT -- the first exponent of an ordinal
O-INFP -- recognizes if an ordinal is infinite
O-P -- a recognizer for the ordinals up to epsilon-0
O-RST -- returns the rest of an infinite ordinal
O< -- the well-founded less-than relation on ordinals up to epsilon-0
O<= -- the less-than-or-equal relation for the ordinals
O> -- the greater-than relation for the ordinals
O>= -- the greater-than-or-equal relation for the ordinals
OBDD -- ordered binary decision diagrams with rewriting
OBSERVATION -- print an observation
OBSERVATION-CW -- See observation.
ODDP -- test whether an integer is odd
OK-IF -- conditional exit from break-rewrite
OOPS -- undo a :u or :ubt
OPEN-INPUT-CHANNEL -- See io.
OPEN-INPUT-CHANNEL-P -- See io.
OPEN-OUTPUT-CHANNEL -- See io.
OPEN-OUTPUT-CHANNEL! -- when trust tags are needed to open output channels
OPEN-OUTPUT-CHANNEL-P -- See io.
OPEN-TRACE-FILE -- redirect trace output to a file
OPTIMIZE -- See declare.
OR -- disjunction
ORACLE-APPLY -- call a function argument on the given list of arguments
ORACLE-APPLY-RAW -- call a function argument on the given list of arguments, no restrictions
ORACLE-FUNCALL -- call a function argument on the remaining arguments
ORDINALS -- ordinals in ACL2
OTF-FLG -- allow more than one initial subgoal to be pushed for induction
OTHER -- other commonly used top-level functions
OUTPUT-TO-FILE -- redirecting output to a file
OVERRIDE-HINTS -- a list of hints given priority in every proof attempt
On the Naming of Subgoals -- On the Naming of Subgoals
Other Requirements -- Other Requirements
Overview of the Expansion of ENDP in the Base Case -- Overview of the Expansion of ENDP in the Base Case
Overview of the Expansion of ENDP in the Induction Step -- Overview of the Expansion of ENDP in the Induction Step
Overview of the Final Simplification in the Base Case -- Overview of the Final Simplification in the Base Case
Overview of the Proof of a Trivial Consequence -- Overview of the Proof of a Trivial Consequence
Overview of the Simplification of the Base Case to T -- Overview of the Simplification of the Base Case to T
Overview of the Simplification of the Induction Conclusion -- Overview of the Simplification of the Induction Conclusion
Overview of the Simplification of the Induction Step to T -- Overview of the Simplification of the Induction Step to T
P! -- to pop up (at least) one level of ACL2's command loop
PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS -- re-defining undone defpkgs
PAIRLIS -- See pairlis$
PAIRLIS$ -- zipper together two lists
PAND -- parallel, Boolean version of and
PARALLEL -- evaluating forms in parallel
PARALLEL-EXECUTION -- for ACL2(p): configure parallel execution
PARALLEL-PROGRAMMING -- parallel programming in ACL2(p)
PARALLEL-PROOF -- parallel proof in ACL2(p)
PARALLEL-PUSHING-OF-SUBGOALS-FOR-INDUCTION -- consequences of how parallelized proofs of subgoals are pushed for induction
PARALLELISM -- experimental extension for parallel execution and proofs
PARALLELISM-AT-THE-TOP-LEVEL -- parallel execution in the ACL2 top-level loop
PARALLELISM-BUILD -- building an ACL2 executable with parallel execution enabled
PARALLELISM-PERFORMANCE -- performance issues for parallel execution
PARALLELISM-TUTORIAL -- a tutorial on how to use the parallelism library.
PARGS -- parallel evaluation of arguments in a function call
PATHNAME -- introduction to filename conventions in ACL2
PBT -- print the commands back through a command descriptor
PC -- print the command described by a command descriptor
PCB -- print the command block described by a command descriptor
PCB! -- print in full the command block described by a command descriptor
PCS -- print the sequence of commands between two command descriptors
PE -- print the events named by a logical name
PE! -- deprecated (see pe)
PEEK-CHAR$ -- See io.
PF -- print the formula corresponding to the given name
PKG-IMPORTS -- list of symbols imported into a given package
PKG-WITNESS -- return a specific symbol in the indicated package
PL -- print the rules for the given name or term
PL2 -- print rule(s) for the given form
PLET -- parallel version of let
PLUSP -- test whether a number is positive
POR -- parallel, Boolean version of or
PORTCULLIS -- the gate guarding the entrance to a certified book
POSITION -- position of an item in a string or a list
POSITION-EQ -- See position.
POSITION-EQUAL -- See position.
POSP -- a recognizer for the positive integers
POST-INDUCTION-KEY-CHECKPOINTS -- reading post-induction key checkpoints
PPROGN -- evaluate a sequence of forms that return state
PR -- print the rules stored by the event with the given name
PR! -- print rules stored by the command with a given command descriptor
PRACTICE-FORMULATING-STRONG-RULES -- a few simple checkpoints suggesting strong rules
PRACTICE-FORMULATING-STRONG-RULES-1 -- rules suggested by (TRUE-LISTP (APPEND (FOO A) (BAR B)))
PRACTICE-FORMULATING-STRONG-RULES-2 -- rules suggested by (TRUE-LISTP (REV (FOO A)))
PRACTICE-FORMULATING-STRONG-RULES-3 -- rules suggested by (MEMBER (FOO A) (APPEND (BAR B) (MUM C)))
PRACTICE-FORMULATING-STRONG-RULES-4 -- rules suggested by (SUBSETP (APPEND (FOO A) (BAR B)) (MUM C))
PRACTICE-FORMULATING-STRONG-RULES-5 -- rules suggested by (SUBSETP (FOO A) (APPEND (BAR B) (MUM C)))
PRACTICE-FORMULATING-STRONG-RULES-6 -- rules suggested by (MEMBER (FOO A) (NATS-BELOW (BAR B)))
PRINC$ -- print an atom
PRINT-CONTROL -- advanced controls of ACL2 printing
PRINT-DOC-START-COLUMN -- printing the one-liner
PRINT-GV -- print a form whose evaluation caused a guard violation
PRINT-OBJECT$ -- See io.
PRINTING-TO-STRINGS -- printing to strings instead of files or standard output
PROFILE -- turn on profiling for one function
PROG2$ -- execute two forms and return the value of the second one
PROGN -- evaluate some events
PROGN! -- evaluate some forms, not necessarily events
PROGN$ -- execute a sequence of forms and return the value of the last one
PROGRAM -- to set the default defun-mode to :program
PROGRAMMING -- programming in ACL2
PROGRAMMING-KNOWLEDGE-TAKEN-FOR-GRANTED -- background knowledge in ACL2 programming for theorem prover tutorial
PROGRAMMING-WITH-STATE -- programming using the von Neumannesque ACL2 state object
PROMPT -- the prompt printed by ld
PROOF-CHECKER -- support for low-level interaction
PROOF-CHECKER-COMMANDS -- list of commands for the proof-checker
PROOF-OF-WELL-FOUNDEDNESS -- a proof that o< is well-founded on o-ps
PROOF-SUPPORTERS-ALIST -- See dead-events.
PROOF-TREE -- proof tree displays
PROOF-TREE-DETAILS -- proof tree details not covered elsewhere
PROOF-TREE-EXAMPLES -- proof tree example
PROOFS-CO -- the proofs character output channel
PROPER-CONSP -- recognizer for proper (null-terminated) non-empty lists
PROPS -- print the ACL2 properties on a symbol
PROVISIONAL-CERTIFICATION -- certify a book in stages for improved parallelism
PSEUDO-TERMP -- a predicate for recognizing term-like s-expressions
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
PUFF -- replace a compound command by its immediate subevents
PUFF* -- replace a compound command by its subevents
PUSH-UNTOUCHABLE -- add name or list of names to the list of untouchable symbols
PUT-ASSOC -- modify an association list by associating a value with a key
PUT-ASSOC-EQ -- See put-assoc.
PUT-ASSOC-EQL -- See put-assoc.
PUT-ASSOC-EQUAL -- See put-assoc.
PUTPROP -- update fast property lists
Pages Written Especially for the Tours -- Pages Written Especially for the Tours
Perhaps -- Perhaps
Popping out of an Inductive Proof -- Popping out of an Inductive Proof
Proving Theorems about Models -- Proving Theorems about Models
Q -- quit ACL2 (type :q) -- reenter with (lp)
QUANTIFIER-TUTORIAL -- A Beginner's Guide to Reasoning about Quantification in ACL2
QUANTIFIERS -- issues about quantification in ACL2
QUANTIFIERS-USING-DEFUN-SK -- quantification example
QUANTIFIERS-USING-DEFUN-SK-EXTENDED -- quantification example with details
QUANTIFIERS-USING-RECURSION -- recursion for implementing quantification
QUIT -- quit entirely out of Lisp
QUOTE -- create a constant
R-EQLABLE-ALISTP -- recognizer for a true list of pairs whose cdrs are suitable for eql
R-SYMBOL-ALISTP -- recognizer for association lists with symbols as values
RANDOM$ -- obtain a random value
RASSOC -- look up value in association list
RASSOC-EQ -- See rassoc.
RASSOC-EQUAL -- See rassoc.
RATIONAL-LISTP -- recognizer for a true list of rational numbers
RATIONALP -- recognizer for rational numbers (ratios and integers)
READ-BYTE$ -- See io.
READ-CHAR$ -- See io.
READ-OBJECT -- See io.
READ-RUN-TIME -- read elapsed runtime
REAL -- ACL2(r) support for real numbers
REAL-LISTP -- ACL2(r) recognizer for a true list of real numbers
REAL/RATIONALP -- recognizer for rational numbers (including real number in ACL2(r))
REALFIX -- coerce to a real number
REALPART -- real part of a complex number
REBUILD -- a convenient way to reconstruct your old state
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
REDEFINING-PROGRAMS -- an explanation of why we restrict redefinitions
REDO-FLAT -- redo on failure of a progn, encapsulate, or certify-book
REDUNDANT-EVENTS -- allowing a name to be introduced ``twice''
REFINEMENT -- record that one equivalence relation refines another
REGENERATE-TAU-DATABASE -- regenerate the tau database relative to the current enabled theory
REGRESSION -- running regressions using the ACL2 community books
RELEASE-NOTES -- pointers to what has changed
REM -- remainder using truncate
REMOVE -- remove all occurrences
REMOVE-BINOP -- remove the association of a function name with a macro name
REMOVE-CUSTOM-KEYWORD-HINT -- remove a custom keyword hint
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-DUPLICATES -- remove duplicates from a string or a list
REMOVE-DUPLICATES-EQ -- See remove-duplicates.
REMOVE-DUPLICATES-EQUAL -- See remove-duplicates.
REMOVE-EQ -- See remove.
REMOVE-EQUAL -- See remove.
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-RAW-ARITY -- remove arity information for raw mode
REMOVE-UNTOUCHABLE -- remove names from lists of untouchable symbols
REMOVE1 -- remove first occurrences, testing using eql
REMOVE1-EQ -- See remove1.
REMOVE1-EQUAL -- See remove1.
REORDER -- hints keyword :REORDER
RESET-FC-REPORTING -- reset the forward-chaining tracking state to its initial configuration
RESET-KILL-RING -- save memory by resetting and perhaps resizing the kill ring used by oops
RESET-LD-SPECIALS -- restores initial settings of the ld specials
RESET-PREHISTORY -- reset the prehistory
RESET-PRINT-CONTROL -- See print-control.
RESIZE-LIST -- list resizer in support of stobjs
REST -- rest (cdr) of the list
RESTORE-MEMOIZATION-SETTINGS -- restore the saved memoization settings
RESTRICT -- hints keyword :RESTRICT
RETRIEVE -- re-enter a (specified) proof-checker state
RETURN-LAST -- return the last argument, perhaps with side effects
RETURN-LAST-TABLE -- install special raw Lisp behavior
REVAPPEND -- concatentate the reverse of one list to another
REVERSE -- reverse a list or string
REWRITE -- make some :rewrite rules (possibly conditional ones)
REWRITE-STACK-LIMIT -- limiting the stack depth of the ACL2 rewriter
RFIX -- coerce to a rational number
ROUND -- division returning an integer by rounding off
RULE-CLASSES -- adding rules to the database
RULE-NAMES -- How rules are named.
RULER-EXTENDERS -- control for ACL2's termination and induction analyses
RUNE -- a rule name
Revisiting the Admission of App -- Revisiting the Admission of App
Rewrite Rules are Generated from DEFTHM Events -- Rewrite Rules are Generated from DEFTHM Events
Running Models -- Running Models
SAVE-AND-CLEAR-MEMOIZATION-SETTINGS -- save and remove the current memoization settings
SAVE-EXEC -- save an executable image and (for most Common Lisps) a wrapper script
SAVING-AND-RESTORING -- saving and restoring your logical state
SEARCH -- search for a string or list in another string or list
SECOND -- second member of the list
SERIALIZE -- routines for saving ACL2 objects to files, and later restoring them
SERIALIZE-ALTERNATIVES -- alternatives to the serialize routines
SERIALIZE-IN-BOOKS -- using serialization efficiently in books
SERIALIZE-READ -- read a serialized ACL2 object from a file
SERIALIZE-WRITE -- write an ACL2 object into a file
SET-ABSSTOBJ-DEBUG -- obtain debugging information upon atomicity violation for an abstract stobj
SET-ACCUMULATED-PERSISTENCE -- See accumulated-persistence.
SET-BACKCHAIN-LIMIT -- sets the backchain-limit used by the type-set and rewriting mechanisms
SET-BODY -- set the definition body
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-CBD -- to set the connected book directory
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-DIFFERENCE$ -- elements of one list that are not elements of another
SET-DIFFERENCE-EQ -- See set-difference$.
SET-DIFFERENCE-EQUAL -- See set-difference$.
SET-DIFFERENCE-THEORIES -- difference of two theories
SET-ENFORCE-REDUNDANCY -- require most events to be redundant
SET-EVISC-TUPLE -- control suppression of details when printing
SET-FC-CRITERIA -- to set the tracking criteria for forward chaining reports
SET-FC-REPORT-ON-THE-FLY -- to determine when forward-chaining reports are printed
SET-FMT-HARD-RIGHT-MARGIN -- set the right margin for formatted output
SET-FMT-SOFT-RIGHT-MARGIN -- set the soft right margin for formatted output
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-IPRINT -- control whether abbreviated output can be read back in
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-BASE -- control radix in which numbers are printed
SET-PRINT-CASE -- control whether symbols are printed in upper case or in lower case
SET-PRINT-CIRCLE -- See print-control.
SET-PRINT-CLAUSE-IDS -- cause subgoal numbers to be printed when 'prove output is inhibited
SET-PRINT-ESCAPE -- See print-control.
SET-PRINT-LENGTH -- See print-control.
SET-PRINT-LEVEL -- See print-control.
SET-PRINT-LINES -- See print-control.
SET-PRINT-RADIX -- control printing of the radix for numbers
SET-PRINT-READABLY -- See print-control.
SET-PRINT-RIGHT-MARGIN -- See print-control.
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-SERIALIZE-CHARACTER -- See with-serialize-character.
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-TRACE-EVISC-TUPLE -- set the trace evisc tuple
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-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
SET-WRITE-ACL2X -- cause certify-book to write out a .acl2x file
SETENV$ -- set an environment variable
SEVENTH -- seventh member of the list
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.
SHOW-BDD -- inspect failed BDD proof attempts
SHOW-BODIES -- show the potential definition bodies
SHOW-CUSTOM-KEYWORD-HINT-EXPANSION -- print out custom keyword hints when they are expanded
SHOW-FC-CRITERIA -- print the forward-chaining tracking criteria
SIGNATURE -- how to specify the arity of a constrained function
SIGNUM -- indicator for positive, negative, or zero
SIMPLE -- :definition and :rewrite rules used in preprocessing
SINGLE-THREADED-OBJECTS -- See stobj.
SIXTH -- sixth member of the list
SKIP-PROOFS -- skip proofs for a given form -- a quick way to introduce unsoundness
SLOW-ALIST-WARNING -- warnings issued when fast-alists are used inefficiently
SLOW-ARRAY-WARNING -- a warning or error issued when arrays are used inefficiently
SOLUTION-TO-SIMPLE-EXAMPLE -- solution to a simple example
SPEC-MV-LET -- modification of mv-let supporting speculative and parallel execution
SPECIAL-CASES-FOR-REWRITE-RULES -- convenient short forms for rewrite rule formulas
SPECIFIC-KINDS-OF-FORMULAS-AS-REWRITE-RULES -- advice about how to handle commonly occurring formulas as rewrite rules
SPECIOUS-SIMPLIFICATION -- nonproductive proof steps
SPLITTER -- reporting of rules whose application may have caused case splits
SPLITTER-OUTPUT -- status for reporting of splitter rules
STANDARD-CHAR-LISTP -- recognizer for a true list of standard characters
STANDARD-CHAR-P -- recognizer for standard characters
STANDARD-CO -- the character output channel to which ld prints
STANDARD-OI -- the standard object input ``channel''
STANDARD-PART -- ACL2(r) function mapping limited numbers to standard numbers
STANDARD-STRING-ALISTP -- recognizer for association lists with standard strings as keys
STANDARDP -- ACL2(r) recognizer for standard objects
START-PROOF-TREE -- start displaying proof trees during proofs
STARTUP -- How to start using ACL2; the ACL2 command loop
STATE -- the von Neumannesque ACL2 state object
STATE-GLOBAL-LET* -- bind state global variables
STOBJ -- single-threaded objects or ``von Neumann bottlenecks''
STOBJ-EXAMPLE-1 -- an example of the use of single-threaded objects
STOBJ-EXAMPLE-1-DEFUNS -- the defuns created by the counters stobj
STOBJ-EXAMPLE-1-IMPLEMENTATION -- the implementation of the counters stobj
STOBJ-EXAMPLE-1-PROOFS -- some proofs involving the counters stobj
STOBJ-EXAMPLE-2 -- an example of the use of arrays in single-threaded objects
STOBJ-EXAMPLE-3 -- another example of a single-threaded object
STOBJS -- xargs keyword :STOBJS
STOP-PROOF-TREE -- stop displaying proof trees during proofs
STRING -- coerce to a string
STRING-APPEND -- concatenate two strings
STRING-DOWNCASE -- in a given string, turn upper-case characters into lower-case
STRING-EQUAL -- string equality without regard to case
STRING-LISTP -- recognizer for a true list of strings
STRING-UPCASE -- in a given string, turn lower-case characters into upper-case
STRING< -- less-than test for strings
STRING<= -- less-than-or-equal test for strings
STRING> -- greater-than test for strings
STRING>= -- less-than-or-equal test for strings
STRINGP -- recognizer for strings
STRIP-CARS -- collect up all first components of pairs in a list
STRIP-CDRS -- collect up all second components of pairs in a list
STRONG-REWRITE-RULES -- formulating good rewrite rules
SUBLIS -- substitute an alist into a tree
SUBSEQ -- subsequence of a string or list
SUBSETP -- test if every member of one list is a member of the other
SUBSETP-EQ -- See subsetp.
SUBSETP-EQUAL -- See subsetp.
SUBST -- a single substitution into a tree
SUBSTITUTE -- substitute into a string or a list, using eql as test
SUBVERSIVE-INDUCTIONS -- why we restrict encapsulated recursive functions
SUBVERSIVE-RECURSIONS -- why we restrict encapsulated recursive functions
SWITCHES-PARAMETERS-AND-MODES -- a variety of ways to modify the ACL2 environment
SYMBOL-< -- less-than test for symbols
SYMBOL-ALISTP -- recognizer for association lists with symbols as keys
SYMBOL-LISTP -- recognizer for a true list of symbols
SYMBOL-NAME -- the name of a symbol (a string)
SYMBOL-PACKAGE-NAME -- the name of the package of a symbol (a string)
SYMBOLP -- recognizer for symbols
SYNTAX -- the syntax of ACL2 is that of Common Lisp
SYNTAXP -- attach a heuristic filter on a :rewrite, :meta, or :linear rule
SYNTAXP-EXAMPLES -- examples pertaining to syntaxp hypotheses
SYS-CALL -- make a system call to the host operating system
SYS-CALL-STATUS -- exit status from the preceding system call
Subsumption of Induction Candidates in App Example -- Subsumption of Induction Candidates in App Example
Suggested Inductions in the Associativity of App Example -- Suggested Inductions in the Associativity of App Example
Symbolic Execution of Models -- Symbolic Execution of Models
TABLE -- user-managed tables
TAKE -- initial segment of a list
TAU-DATA -- to see what tau knows about a function symbol
TAU-DATABASE -- to see the tau database as a (very large) object
TAU-INTERVAL-DOM -- access the domain of a tau interval
TAU-INTERVAL-HI -- access the upper bound of a tau interval
TAU-INTERVAL-HI-REL -- access the upper bound relation of a tau interval
TAU-INTERVAL-LO -- access the lower bound of a tau interval
TAU-INTERVAL-LO-REL -- access the lower bound relation of a tau interval
TAU-INTERVALP -- Boolean recognizer for tau intervals
TAU-STATUS -- query or set tau system status
TAU-SYSTEM -- make a rule for the ACL2 ``type checker''
TENTH -- tenth member of the list
TERM -- the three senses of well-formed ACL2 expressions or formulas
TERM-ORDER -- the ordering relation on terms used by ACL2
TERM-TABLE -- a table used to validate meta rules
THE -- run-time type check
THE-METHOD -- how to find proofs
THEORIES -- sets of runes to enable/disable in concert
THEORIES-AND-PRIMITIVES -- warnings from disabling certain built-in functions
THEORY -- retrieve named theory
THEORY-FUNCTIONS -- functions for obtaining or producing theories
THEORY-INVARIANT -- user-specified invariants on theories
THIRD -- third member of the list
THM -- prove a theorem
TIDBITS -- some basic hints for using ACL2
TIME$ -- time an evaluation
TIME-TRACKER -- display time spent during specified evaluation
TIME-TRACKER-TAU -- messages about expensive use of the tau-system
TIPS -- some hints for using the ACL2 prover
TOGGLE-PC-MACRO -- change an ordinary macro command to an atomic macro, or vice-versa
TOP-LEVEL -- evaluate a top-level form as a function body
TRACE -- tracing functions in ACL2
TRACE! -- trace the indicated functions after creating an active trust tag
TRACE$ -- trace function evaluations
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
TRUE-LIST-LISTP -- recognizer for true (proper) lists of true lists
TRUE-LISTP -- recognizer for proper (null-terminated) lists
TRUNCATE -- division returning an integer by truncating toward 0
TRUST-TAG -- See defttag.
TTAGS-SEEN -- list some declared trust tags (ttags)
TTREE -- tag-trees
TUTORIAL1-TOWERS-OF-HANOI -- The Towers of Hanoi Example
TUTORIAL2-EIGHTS-PROBLEM -- The Eights Problem Example
TUTORIAL3-PHONEBOOK-EXAMPLE -- A Phonebook Specification
TUTORIAL4-DEFUN-SK-EXAMPLE -- example of quantified notions
TUTORIAL5-MISCELLANEOUS-EXAMPLES -- miscellaneous ACL2 examples
TYPE -- See declare.
TYPE-PRESCRIPTION -- make a rule that specifies the type of a term
TYPE-SET -- how type information is encoded in ACL2
TYPE-SET-INVERTER -- exhibit a new decoding for an ACL2 type-set
TYPE-SPEC -- type specifiers in declarations
The Admission of App -- The Admission of App
The Associativity of App -- The Associativity of App
The Base Case in the App Example -- The Base Case in the App Example
The End of the Flying Tour -- The End of the Flying Tour
The End of the Proof of the Associativity of App -- The End of the Proof of the Associativity of App
The End of the Walking Tour -- The End of the Walking Tour
The Event Summary -- The Event Summary
The Expansion of ENDP in the Induction Step (Step 0) -- The Expansion of ENDP in the Induction Step (Step 0)
The Expansion of ENDP in the Induction Step (Step 1) -- The Expansion of ENDP in the Induction Step (Step 1)
The Expansion of ENDP in the Induction Step (Step 2) -- The Expansion of ENDP in the Induction Step (Step 2)
The Falling Body Model -- The Falling Body Model
The Final Simplification in the Base Case (Step 0) -- the Final Simplification in the Base Case (Step 0)
The Final Simplification in the Base Case (Step 1) -- the Final Simplification in the Base Case (Step 1)
The Final Simplification in the Base Case (Step 2) -- the Final Simplification in the Base Case (Step 2)
The Final Simplification in the Base Case (Step 3) -- the Final Simplification in the Base Case (Step 3)
The First Application of the Associativity Rule -- The First Application of the Associativity Rule
The Induction Scheme Selected for the App Example -- The Induction Scheme Selected for the App Example
The Induction Step in the App Example -- The Induction Step in the App Example
The Instantiation of the Induction Scheme -- The Instantiation of the Induction Scheme
The Justification of the Induction Scheme -- The Justification of the Induction Scheme
The Proof of the Associativity of App -- The Proof of the Associativity of App
The Q.E.D. Message -- The Q.E.D. Message
The Rules used in the Associativity of App Proof -- The Rules used in the Associativity of App Proof
The Simplification of the Induction Conclusion (Step 0) -- the Simplification of the Induction Conclusion (Step 0)
The Simplification of the Induction Conclusion (Step 1) -- the Simplification of the Induction Conclusion (Step 1)
The Simplification of the Induction Conclusion (Step 10) -- the Simplification of the Induction Conclusion (Step 10)
The Simplification of the Induction Conclusion (Step 11) -- the Simplification of the Induction Conclusion (Step 11)
The Simplification of the Induction Conclusion (Step 12) -- the Simplification of the Induction Conclusion (Step 12)
The Simplification of the Induction Conclusion (Step 2) -- the Simplification of the Induction Conclusion (Step 2)
The Simplification of the Induction Conclusion (Step 3) -- the Simplification of the Induction Conclusion (Step 3)
The Simplification of the Induction Conclusion (Step 4) -- the Simplification of the Induction Conclusion (Step 4)
The Simplification of the Induction Conclusion (Step 5) -- the Simplification of the Induction Conclusion (Step 5)
The Simplification of the Induction Conclusion (Step 6) -- the Simplification of the Induction Conclusion (Step 6)
The Simplification of the Induction Conclusion (Step 7) -- the Simplification of the Induction Conclusion (Step 7)
The Simplification of the Induction Conclusion (Step 8) -- the Simplification of the Induction Conclusion (Step 8)
The Simplification of the Induction Conclusion (Step 9) -- the Simplification of the Induction Conclusion (Step 9)
The Summary of the Proof of the Trivial Consequence -- The Summary of the Proof of the Trivial Consequence
The Theorem that App is Associative -- The Theorem that App is Associative
The Time Taken to do the Associativity of App Proof -- The Time Taken to do the Associativity of App Proof
The Tours -- The Tours
The WARNING about the Trivial Consequence -- The WARNING about the Trivial Consequence
U -- undo last command, without a query
UBT -- undo the commands back through a command descriptor
UBT! -- undo commands, without a query or an error
UBT-PREHISTORY -- undo the commands back through the last reset-prehistory event
UBU -- undo the commands back up to (not including) a command descriptor
UBU! -- undo commands, without a query or an error
UNARY-- -- arithmetic negation function
UNARY-/ -- reciprocal function
UNCERTIFIED-BOOKS -- invalid certificates and uncertified books
UNION$ -- elements of one list that are not elements of another
UNION-EQ -- See union$.
UNION-EQUAL -- See union$.
UNION-THEORIES -- union two theories
UNIVERSAL-THEORY -- all rules as of logical name
UNMEMOIZE -- turn off memoization for the specified function
UNMONITOR -- to stop monitoring a rule name
UNSAVE -- remove a proof-checker state
UNSUPPORTED-PARALLELISM-FEATURES -- ACL2 features not supported in ACL2(p)
UNSUPPORTED-WATERFALL-PARALLELISM-FEATURES -- proof features not supported with waterfall-parallelism enabled
UNTRACE$ -- untrace functions
UNTRANS-TABLE -- associates a function symbol with a macro for printing user-level terms
UNTRANSLATE -- See user-defined-functions-table.
UPDATE-NTH -- modify a list by putting the given value at the given position
UPPER-CASE-P -- recognizer for upper case characters
USE -- hints keyword :USE
USER-DEFINED-FUNCTIONS-TABLE -- an advanced table used to replace certain system functions
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
USING-TABLES-EFFICIENTLY -- Notes on how to use tables efficiently
Undocumented Topic -- Undocumented Topic
Using the Associativity of App to Prove a Trivial Consequence -- Using the Associativity of App to Prove a Trivial Consequence
VALUE-TRIPLE -- compute a value, optionally checking that it is not nil
VERBOSE-PSTACK -- seeing what is the prover up to (for advanced users)
VERIFY -- enter the interactive proof checker
VERIFY-GUARDS -- verify the guards of a function
VERIFY-GUARDS-EAGERNESS -- See set-verify-guards-eagerness.
VERIFY-GUARDS-FORMULA -- view the guard proof obligation, without proving it
VERIFY-TERMINATION -- convert a function from :program mode to :logic mode
VERSION -- ACL2 Version Number
WALKABOUT -- explore an ACL2 cons tree
WATERFALL -- See hints-and-the-waterfall.
WATERFALL-PARALLELISM -- for ACL2(p): configuring the parallel execution of the waterfall
WATERFALL-PRINTING -- for ACL2(p): configuring the printing within the parallelized waterfall
WELL-FOUNDED-RELATION -- show that a relation is well-founded on a set
WET -- evaluate a form and print subsequent error trace
WHY-BRR -- an explanation of why ACL2 has an explicit brr mode
WITH-FAST-ALIST -- (with-fast-alist name form) causes name to be a fast alist for the
execution of form.
WITH-GUARD-CHECKING -- suppressing or enable guard-checking for a form
WITH-LIVE-STATE -- allow a reference to state in raw Lisp
WITH-LOCAL-STATE -- locally bind state
WITH-LOCAL-STOBJ -- locally bind a single-threaded object
WITH-OUTPUT -- suppressing or turning on specified output for an event
WITH-OUTPUT-LOCK -- provides a mutual-exclusion mechanism for performing output in parallel
WITH-PROVER-STEP-LIMIT -- limit the number of steps for proofs
WITH-PROVER-TIME-LIMIT -- limit the time for proofs
WITH-SERIALIZE-CHARACTER -- control output mode for print-object$
WITH-STOLEN-ALIST -- (with-stolen-alist name form) ensures that name is a fast alist at the
start of the execution of form. At the end of execution, it ensures that
name is a fast alist if and only if it was originally. That is, if
name was not a fast alist originally, its hash table link is freed, and if
it was a fast alist originally but its table was modified during the execution
of form, that table is restored. Note that any extended table created from
the original fast alist during form must be manually freed.
WITHOUT-EVISC -- print output in full
WOF -- direct standard output and proofs output to a file
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
WRITE-BYTE$ -- See io.
What Is ACL2(Q) -- What Is ACL2?
What is Required of the User(Q) -- What is Required of the User?
What is a Mathematical Logic(Q) -- What is a Mathematical Logic?
What is a Mechanical Theorem Prover(Q) -- What is a Mechanical Theorem Prover?
What is a Mechanical Theorem Prover(Q) (cont) -- What is a Mechanical Theorem Prover? (cont)
XARGS -- extra arguments, for example to give hints to defun
XOR -- logical ``exclusive or''
You Must Think about the Use of a Formula as a Rule -- You Must Think about the Use of a Formula as a Rule
ZERO-TEST-IDIOMS -- how to test for 0
ZEROP -- test an acl2-number against 0
ZIP -- testing an ``integer'' against 0
ZP -- testing a ``natural'' against 0
ZPF -- testing a nonnegative fixnum against 0
ACL2-PC::= -- (atomic macro)
attempt an equality (or equivalence) substitution
ACL2-PC::ACL2-WRAP -- (macro)
same as (lisp x)
ACL2-PC::ADD-ABBREVIATION -- (primitive)
add an abbreviation
ACL2-PC::AL -- (macro)
same as apply-linear
ACL2-PC::APPLY-LINEAR -- (primitive)
apply a linear rule
ACL2-PC::BASH -- (atomic macro)
call the ACL2 theorem prover's simplifier
ACL2-PC::BDD -- (atomic macro)
prove the current goal using bdds
ACL2-PC::BK -- (atomic macro)
move backward one argument in the enclosing term
ACL2-PC::BOOKMARK -- (macro)
insert matching ``bookends'' comments
ACL2-PC::CASESPLIT -- (primitive)
split into two cases
ACL2-PC::CG -- (macro)
change to another goal.
ACL2-PC::CHANGE-GOAL -- (primitive)
change to another goal.
ACL2-PC::CL-PROC -- (macro)
same as clause-processor
ACL2-PC::CLAIM -- (atomic macro)
add a new hypothesis
ACL2-PC::CLAUSE-PROCESSOR -- (atomic macro)
use a clause-processor
ACL2-PC::COMM -- (macro)
display instructions from the current interactive session
ACL2-PC::COMMANDS -- (macro)
display instructions from the current interactive session
ACL2-PC::COMMENT -- (primitive)
insert a comment
ACL2-PC::CONTRADICT -- (macro)
same as contrapose
ACL2-PC::CONTRAPOSE -- (primitive)
switch a hypothesis with the conclusion, negating both
ACL2-PC::DEMOTE -- (primitive)
move top-level hypotheses to the conclusion
ACL2-PC::DIVE -- (primitive)
move to the indicated subterm
ACL2-PC::DO-ALL -- (macro)
run the given instructions
ACL2-PC::DO-ALL-NO-PROMPT -- (macro)
run the given instructions, halting once there is a ``failure''
ACL2-PC::DO-STRICT -- (macro)
run the given instructions, halting once there is a ``failure''
ACL2-PC::DROP -- (primitive)
drop top-level hypotheses
ACL2-PC::DV -- (atomic macro)
move to the indicated subterm
ACL2-PC::ELIM -- (atomic macro)
call the ACL2 theorem prover's elimination process
ACL2-PC::EQUIV -- (primitive)
attempt an equality (or congruence-based) substitution
ACL2-PC::EX -- (macro)
exit after possibly saving the state
ACL2-PC::EXIT -- (meta)
exit the interactive proof-checker
ACL2-PC::EXPAND -- (primitive)
expand the current function call without simplification
ACL2-PC::FAIL -- (macro)
cause a failure
ACL2-PC::FINISH -- (macro)
require completion of instructions; save error if inside :hints
ACL2-PC::FORWARDCHAIN -- (atomic macro)
forward chain from an implication in the hyps
ACL2-PC::FREE -- (atomic macro)
create a ``free variable''
ACL2-PC::GENEQV -- (macro)
show the generated equivalence relation maintained at the current subterm
ACL2-PC::GENERALIZE -- (primitive)
perform a generalization
ACL2-PC::GOALS -- (macro)
list the names of goals on the stack
ACL2-PC::HELP -- (macro)
proof-checker help facility
ACL2-PC::HELP! -- (macro)
proof-checker help facility
ACL2-PC::HELP-LONG -- (macro)
same as help!
ACL2-PC::HYPS -- (macro)
print the hypotheses
ACL2-PC::ILLEGAL -- (macro)
illegal instruction
ACL2-PC::IN-THEORY -- (primitive)
set the current proof-checker theory
ACL2-PC::INDUCT -- (atomic macro)
generate subgoals using induction
ACL2-PC::LEMMAS-USED -- (macro)
print the runes (definitions, lemmas, ...) used
ACL2-PC::LISP -- (meta)
evaluate the given form in Lisp
ACL2-PC::MORE -- (macro)
proof-checker help facility
ACL2-PC::MORE! -- (macro)
proof-checker help facility
ACL2-PC::NEGATE -- (macro)
run the given instructions, and ``succeed'' if and only if they ``fail''
ACL2-PC::NIL -- (macro)
used for interpreting control-d
ACL2-PC::NOISE -- (meta)
run instructions with output
ACL2-PC::NX -- (atomic macro)
move forward one argument in the enclosing term
ACL2-PC::ORELSE -- (macro)
run the first instruction; if (and only if) it ``fails'', run the
second
ACL2-PC::P -- (macro)
prettyprint the current term
ACL2-PC::P-TOP -- (macro)
prettyprint the conclusion, highlighting the current term
ACL2-PC::PL -- (macro)
print the rules for a given name
ACL2-PC::PP -- (macro)
prettyprint the current term
ACL2-PC::PR -- (macro)
print the rules for a given name
ACL2-PC::PRINT -- (macro)
print the result of evaluating the given form
ACL2-PC::PRINT-ALL-CONCS -- (macro)
print all the conclusions of (as yet unproved) goals
ACL2-PC::PRINT-ALL-GOALS -- (macro)
print all the (as yet unproved) goals
ACL2-PC::PRINT-MAIN -- (macro)
print the original goal
ACL2-PC::PRO -- (atomic macro)
repeatedly apply promote
ACL2-PC::PROMOTE -- (primitive)
move antecedents of conclusion's implies term to top-level
hypotheses
ACL2-PC::PROTECT -- (macro)
run the given instructions, reverting to existing state upon
failure
ACL2-PC::PROVE -- (primitive)
call the ACL2 theorem prover to prove the current goal
ACL2-PC::PSO -- (macro)
print the most recent proof attempt from inside the proof-checker
ACL2-PC::PSO! -- (macro)
print the most recent proof attempt from inside the proof-checker
ACL2-PC::PSOG -- (macro)
print the most recent proof attempt from inside the proof-checker
ACL2-PC::PUT -- (macro)
substitute for a ``free variable''
ACL2-PC::QUIET -- (meta)
run instructions without output
ACL2-PC::R -- (macro)
same as rewrite
ACL2-PC::REDUCE -- (atomic macro)
call the ACL2 theorem prover's simplifier
ACL2-PC::REDUCE-BY-INDUCTION -- (macro)
call the ACL2 prover without induction, after going into
induction
ACL2-PC::REMOVE-ABBREVIATIONS -- (primitive)
remove one or more abbreviations
ACL2-PC::REPEAT -- (macro)
repeat the given instruction until it ``fails''
ACL2-PC::REPEAT-REC -- (macro)
auxiliary to repeat
ACL2-PC::REPLAY -- (macro)
replay one or more instructions
ACL2-PC::RESTORE -- (meta)
remove the effect of an UNDO command
ACL2-PC::RETAIN -- (atomic macro)
drop all but the indicated top-level hypotheses
ACL2-PC::RETRIEVE -- (macro)
re-enter the proof-checker
ACL2-PC::REWRITE -- (primitive)
apply a rewrite rule
ACL2-PC::RUN-INSTR-ON-GOAL -- (macro)
auxiliary to THEN
ACL2-PC::RUN-INSTR-ON-NEW-GOALS -- (macro)
auxiliary to then
ACL2-PC::RUNES -- (macro)
print the runes (definitions, lemmas, ...) used
ACL2-PC::S -- (primitive)
simplify the current subterm
ACL2-PC::S-PROP -- (atomic macro)
simplify propositionally
ACL2-PC::SAVE -- (macro)
save the proof-checker state (state-stack)
ACL2-PC::SEQUENCE -- (meta)
run the given list of instructions according to a multitude of
options
ACL2-PC::SHOW-ABBREVIATIONS -- (macro)
display the current abbreviations
ACL2-PC::SHOW-LINEARS -- (macro)
display the applicable linear rules
ACL2-PC::SHOW-REWRITES -- (macro)
display the applicable rewrite rules
ACL2-PC::SHOW-TYPE-PRESCRIPTIONS -- (macro)
display the applicable type-prescription rules
ACL2-PC::SKIP -- (macro)
``succeed'' without doing anything
ACL2-PC::SL -- (atomic macro)
simplify with lemmas
ACL2-PC::SLS -- (macro)
same as SHOW-LINEARS
ACL2-PC::SPLIT -- (atomic macro)
split the current goal into cases
ACL2-PC::SR -- (macro)
same as SHOW-REWRITES
ACL2-PC::ST -- (macro)
same as SHOW-TYPE-PRESCRIPTIONS
ACL2-PC::SUCCEED -- (macro)
run the given instructions, and ``succeed''
ACL2-PC::TH -- (macro)
print the top-level hypotheses and the current subterm
ACL2-PC::THEN -- (macro)
apply one instruction to current goal and another to new subgoals
ACL2-PC::TOP -- (atomic macro)
move to the top of the goal
ACL2-PC::TYPE-ALIST -- (macro)
display the type-alist from the current context
ACL2-PC::UNDO -- (meta)
undo some instructions
ACL2-PC::UNSAVE -- (macro)
remove a proof-checker state
ACL2-PC::UP -- (primitive)
move to the parent (or some ancestor) of the current subterm
ACL2-PC::USE -- (atomic macro)
use a lemma instance
ACL2-PC::WRAP -- (atomic macro)
execute the indicated instructions and combine all the new goals
ACL2-PC::WRAP-INDUCT -- (atomic macro)
same as induct, but create a single goal
ACL2-PC::WRAP1 -- (primitive)
combine goals into a single goal
ACL2-PC::X -- (atomic macro)
expand and (maybe) simplify function call at the current subterm
ACL2-PC::X-DUMB -- (atomic macro)
expand function call at the current subterm, without simplifying
