Index

Home

This is an index that alphabetically lists all documented topics. Each may be clicked on, to take you to that topic. * -- 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, symbols, or characters)

> -- greater-than test

>= -- greater-than-or-equal test

@ -- get the value of a global variable in state

ABS -- the absolute value of a rational number

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

ACKNOWLEDGEMENTS -- some contributors to the well-being of ACL2

ACL2-CHARACTERP -- recognizer for characters

ACL2-COMPLEX-RATIONALP -- recognizer for complex rationals

ACL2-COUNT -- a commonly used measure for justifying recursion

ACL2-CUSTOMIZATION -- customizing ACL2 for a particular user

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

ACL2-NUMBERP -- recognizer for numbers

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::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::CLAIM -- (atomic macro)
add a new hypothesis

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::FORWARDCHAIN -- (atomic macro)
forward chain from an implication in the hyps

ACL2-PC::FREE -- (atomic macro)
create a ``free variable''

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::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::PP -- (macro)
prettyprint the current term

ACL2-PC::PRINT -- (macro)
print the result of evaluating the given form

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::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 toxae THEN

ACL2-PC::RUN-INSTR-ON-NEW-GOALS -- (macro)
auxiliary to then

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-REWRITES -- (macro)
display the applicable rewrite rules

ACL2-PC::SKIP -- (macro)
``succeed'' without doing anything

ACL2-PC::SL -- (atomic macro)
simplify with lemmas

ACL2-PC::SPLIT -- (atomic macro)
split the current goal into cases

ACL2-PC::SR -- (macro)
same as SHOW-REWRITES

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

ACL2-TUTORIAL -- tutorial introduction to ACL2

ACL2-USER -- a package the ACL2 user may prefer

ACONS -- constructor for association lists

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

ADD-TO-SET-EQ -- add a symbol to a list

ALISTP -- recognizer for association lists

ALPHA-CHAR-P -- recognizer for alphabetic characters

AND -- conjunction

APPEND -- concatenate two or more lists

APROPOS -- searching :doc and :more-doc text

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.

ASET1 -- set the elements of a 1-dimensional array

ASET2 -- set the elements of a 2-dimensional array

ASH -- arithmetic shift operation

ASSIGN -- assign to a global variable in state

ASSOC -- look up key in association list, using eql as test

ASSOC-EQ -- look up key in association list, using eq as test

ASSOC-EQUAL -- look up key in association list

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

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

BOOK-CONTENTS -- restrictions on the forms inside books

BOOK-EXAMPLE -- how to create, certify, and use a simple book

BOOK-NAME -- conventions associated with book names

BOOKS -- files of ACL2 event forms

BOOLEANP -- recognizer for booleans

BREAK-LEMMA -- a quick introduction to breaking rewrite rules in 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-CLAUSES -- to build in a clause for measure and guard processing

BUTLAST -- all but a final segment of a list

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

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

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-LISTP -- recognizer for a true list of 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

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

COMP -- compile some ACL2 functions

COMPILATION -- compiling ACL2 functions

COMPLEX -- create an ACL2 number

COMPLEX-RATIONALP -- recognizes complex rational 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

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

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

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

CURRENT-THEORY -- currently enabled rules as of logical name

DECLARE -- declarations

DEFAULT -- return the :default from the header of a 1- or 2-dimensional array

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

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

DEFAXIOM -- add an axiom

DEFCHOOSE -- define a Skolem (witnessing) function

DEFCONG -- prove that one equivalence relation preserves another in a given
argument position of a given function

DEFCONST -- define a constant

DEFDOC -- add a documentation topic

DEFEQUIV -- prove that a function is an equivalence relation

DEFEVALUATOR -- introduce an evaluator function

DEFINE-PC-HELP -- define a macro command whose purpose is to print something

DEFINITION -- make a rule that acts like a function definition

DEFLABEL -- build a landmark and/or add a documentation topic

DEFMACRO -- define a macro

DEFPKG -- define a new symbol package

DEFREFINEMENT -- prove that equiv1 refines equiv2

DEFSTUB -- stub-out a function symbol

DEFTHEORY -- define a theory (to enable or disable a set of rules)

DEFTHM -- prove and name a theorem

DEFUN -- define a function symbol

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

DEFUN-MODE-CAVEAT -- functions with defun-mode of :program considered unsound

DEFUN-SK -- define a function whose body has an outermost quantifier

DEFUNS -- an alternative to mutual-recursion

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

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

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 at the terminal

E0-ORD-< -- the well-founded less-than relation on ordinals up to epsilon-0

E0-ORDINALP -- a recognizer for the ordinals up to epsilon-0

EIGHTH -- eighth member of the list

ELIM -- make a destructor elimination rule

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

ENABLE -- adds names to current theory

ENABLE-FORCING -- to allow forced case splits

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

EQUIVALENCE -- mark a relation as an equivalence relation

ER-PROGN -- perform a sequence of state-changing ``error triples''

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

EVENP -- test whether an integer is even

EVENTS -- functions that extend the logic

EVISCERATE-HIDE-TERMS -- to print (hide ...) as <hidden>

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-BOOT-STRAP-MODE -- the end of pre-history

EXPLODE-NONNEGATIVE-INTEGER -- the list of characters in the decimal form of a number

EXPT -- exponential function

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

FAILURE -- how to deal with a proof failure

FIFTH -- fifth member of the list

FILE-READING-EXAMPLE -- example of reading files in ACL2

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

FLOOR -- division returning an integer by truncating toward negative infinity

FMS -- :(str alist co-channel state evisc) => state

FMT -- formatted printing

FMT1 -- :(str alist col co-channel state evisc) => (mv col state)

FORALL -- universal quantifier

FORCE -- identity function used to force a case split

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

FORWARD-CHAINING -- make a rule to forward chain when a certain trigger arises

FOURTH -- fourth member of the list

FULL-BOOK-NAME -- book naming conventions assumed by ACL2

FUNCTION-THEORY -- function symbol rules as of logical name

GENERALIZE -- make a rule to restrict generalizations

GENERALIZED-BOOLEANS -- potential soundness issues related to ACL2 predicates

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

GOOD-BYE -- quit entirely out of Lisp

GROUND-ZERO -- enabled rules in the startup theory

GUARD -- restricting the domain of a function

GUARD-EXAMPLE -- a brief transcript illustrating guards in ACL2

GUARD-INTRODUCTION -- introduction to guards in ACL2

GUARD-MISCELLANY -- miscellaneous remarks about guards

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

HEADER -- return the header of a 1- or 2-dimensional array

HELP -- brief survey of ACL2 features

HIDE -- hide a term from the rewriter

HINTS -- advice to the theorem proving process

HISTORY -- functions that display or change history

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

IDENTITY -- the identity function

IF -- if-then-else function

IF* -- for conditional rewriting with BDDs

IFF -- logical ``if and only if''

IFIX -- coerce to an integer

ILLEGAL -- cause a hard error

IMAGPART -- imaginary part of a complex number

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-PACKAGE -- select current package

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

INDUCTION -- make a rule that suggests a certain induction

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

INTERN -- create a new symbol in a given package

INTERN-IN-PACKAGE-OF-SYMBOL -- create a symbol with a given name

INTERSECTION-THEORIES -- intersect two theories

INTERSECTP-EQ -- test whether two lists of symbols intersect

INTERSECTP-EQUAL -- test whether two lists intersect

INTRODUCTION -- introduction to ACL2

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

IO -- input/output facilities in ACL2

IRRELEVANT-FORMALS -- formals that are used but only insignificantly

KEEP -- how we know if include-book read the correct files

KEYWORD-COMMANDS -- how keyword commands are processed

KEYWORD-VALUE-LISTP -- recognizer for true lists whose even-position elements are keywords

KEYWORDP -- recognizer for keywords

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

LENGTH -- length of a string or proper list

LET -- binding of lexically scoped (local) variables

LET* -- binding of lexically scoped (local) variables

LINEAR -- make some arithmetic inequality rules

LINEAR-ALIAS -- make a rule to extend the applicability of linear arithmetic

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 two 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 two integers

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

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

LOGIOR -- bitwise logical inclusive or of two 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 two 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-LIST -- make a list of a given size

MARKUP -- the markup language for ACL2 documentation strings

MAX -- the larger of two rational numbers

MAXIMUM-LENGTH -- return the :maximum-length from the header of an array

MEMBER -- membership predicate, using eql as test

MEMBER-EQ -- membership predicate, using eq as test

MEMBER-EQUAL -- membership predicate

META -- make a :meta rule (a hand-written simplifier)

MIN -- the smaller of two rational numbers

MINUSP -- test whether a rational number is negative

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

MOD -- remainder using floor

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-doc's ``(cont'd)''

MORE! -- another response to ``(cont'd)''

MORE-DOC -- a continuation of the :doc documentation

MUTUAL-RECURSION -- define some mutually recursive functions

MUTUAL-RECURSION-PROOF-EXAMPLE -- a small proof about mutually recursive functions

MV -- returning multiple values

MV-LET -- calling multi-valued ACL2 functions

MV-NTH -- the mv-nth element (zero-based) of a list

NAME -- syntactic rules on logical names

NFIX -- coerce to a natural number

NINTH -- ninth member of the list

NO-DUPLICATESP -- check for duplicates in a list

NONNEGATIVE-INTEGER-QUOTIENT -- natural number division function

NOT -- logical negation

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

NQTHM-TO-ACL2 -- ACL2 analogues of Nqthm functions and commands

NTH -- the nth element (zero-based) of a list

NTHCDR -- final segment of a list

NULL -- recognizer for the empty list

NUMERATOR -- dividend of a ratio in lowest terms

OBDD -- ordered binary decision diagrams with rewriting

ODDP -- test whether an integer is odd

OK-IF -- conditional exit from break-rewrite

OOPS -- undo a :u or :ubt

OR -- conjunction

OTF-FLG -- pushing all the initial subgoals

OTHER -- other commonly used top-level functions

PACKAGE-REINCARNATION-IMPORT-RESTRICTIONS -- re-defining undone defpkgs

PAIRLIS -- see pairlis$

PAIRLIS$ -- zipper together two lists

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 event named by a logical name

PE! -- print all the events named by a logical name

PF -- print the formula corresponding to the given name

PL -- print the rules whose top function symbol is the given name

PLUSP -- test whether a rational number is positive

PORTCULLIS -- the gate guarding the entrance to a certified book

POSITION -- position of an item in a string or a list, using eql as test

POSITION-EQ -- position of an item in a string or a list, using eq as test

POSITION-EQUAL -- position of an item in a string or a list

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

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

PROGN -- see the documentation for er-progn

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

PROGRAMMING -- built-in ACL2 functions

PROMPT -- the prompt printed by ld

PROOF-CHECKER -- support for low-level interaction

PROOF-OF-WELL-FOUNDEDNESS -- a proof that e0-ord-< is well-founded on e0-ordinalps

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

PSEUDO-TERMP -- a predicate for recognizing term-like s-expressions

PUFF -- replace a compound command by its immediate subevents

PUFF* -- replace a compound command by its subevents

PUT-ASSOC-EQ -- modify an association list by associating a value with a key

PUT-ASSOC-EQUAL -- modify an association list by associating a value with a key

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

RASSOC -- look up value in association list, using eql as test

RATIONAL-LISTP -- recognizer for a true list of rational numbers

RATIONALP -- recognizer for whole numbers

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! -- system hacker's redefinition command

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

REDEFINING-PROGRAMS -- an explanation of why we restrict redefinitions

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

REFINEMENT -- record that one equivalence relation refines another

RELEASE-NOTES -- pointers to what has changed

REM -- remainder using truncate

REMOVE -- remove all occurrences, testing using eql

REMOVE-DUPLICATES -- remove duplicates from a string or (using eql) a list

REMOVE-DUPLICATES-EQUAL -- remove duplicates from a list

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

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

REST -- rest (cdr) of the list

RETRIEVE -- re-enter a (specified) proof-checker state

REVAPPEND -- concatentate the reverse of one list to another

REVERSE -- reverse a list

REWRITE -- make some :rewrite rules (possibly conditional ones)

RFIX -- coerce to a rational number

ROUND -- division returning an integer by rounding off

RULE-CLASSES -- adding rules to the data base

RULE-NAMES -- How rules are named.

RUNE -- a rule name

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

SECOND -- second member of the list

SET-CBD -- to set the connected book directory

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

SET-DIFFERENCE-EQUAL -- elements of one list that are not elements of another

SET-DIFFERENCE-THEORIES -- difference of two theories

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

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

SET-INHIBIT-OUTPUT-LST -- control output

SET-INHIBIT-WARNINGS -- control warnings

SET-INVISIBLE-FNS-ALIST -- set the invisible functions alist

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

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

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

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

SEVENTH -- seventh member of the list

SHOW-BDD -- inspect failed BDD proof attempts

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

SIXTH -- sixth member of the list

SKIP-PROOFS -- skip proofs for an event -- a quick way to introduce unsoundness

SLOW-ARRAY-WARNING -- a warning issued when arrays are used inefficiently

SOLUTION-TO-SIMPLE-EXAMPLE -- solution to a simple example

SPECIOUS-SIMPLIFICATION -- nonproductive proof steps

STANDARD-CHAR-LISTP -- recognizer for 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''

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

STOP-PROOF-TREE -- stop displaying proof trees during proofs

STRING -- coerce to a string

STRING-ALISTP -- recognizer for association lists with strings as keys

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

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-EQUAL -- check if all members of one list are members of the other

SUBST -- a single substitution into a tree

SUBVERSIVE-INDUCTIONS -- why we restrict encapsulated recursive functions

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 -- to attach a heuristic filter on a :rewrite rule

TABLE -- user-managed tables

TAKE -- initial segment of a list

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

THEORIES -- sets of runes to enable/disable in concert

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

TIPS -- some hints for using the ACL2 prover

TOGGLE-PC-MACRO -- change an ordinary macro command to an atomic macro, or vice-versa

TRANS -- print the macroexpansion of a form

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

TUTORIAL-EXAMPLES -- examples of ACL2 usage

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

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

UNARY-- -- arithmetic negation function

UNARY-/ -- reciprocal function

UNCERTIFIED-BOOKS -- invalid certificates and uncertified books

UNION-EQ -- union of two lists of symbols

UNION-EQUAL -- union of two lists

UNION-THEORIES -- union two theories

UNIVERSAL-THEORY -- all rules as of logical name

UNMONITOR -- to stop monitoring a rule name

UNSAVE -- remove a proof-checker state

UPDATE-NTH -- modify a list by putting the given value at the given position

UPPER-CASE-P -- recognizer for upper case characters

VERIFY -- enter the interactive proof checker

VERIFY-GUARDS -- verify the guards of a function

VERIFY-TERMINATION -- convert a function from :program mode to :logic mode

WELL-FOUNDED-RELATION -- show that a relation is well-founded on a set

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

WORLD -- ACL2 property lists and the ACL2 logical data base

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

XARGS -- giving hints to defun

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