PROGRAMMING

Major Section:  ACL2 Documentation

The built-in ACL2 functions that one typically uses in writing programs are listed below. See their individual documentations. We do not bother to document the some of the more obscure functions provided by ACL2 that do not correspond to functions of Common Lisp.

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

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

• ABS -- the absolute value of a real number

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

• ACL2-NUMBERP -- recognizer for numbers

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

• ACONS -- constructor for association lists

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

• ADD-TO-SET-EQL -- add an object to a list

• ADD-TO-SET-EQUAL -- add an object to a list

• 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

• AND -- conjunction

• APPEND -- concatenate two or more lists

• ARRAYS -- an introduction to ACL2 arrays.

• ASH -- arithmetic shift operation

• ASSERT$ -- cause a hard error if the given test is false

• 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

• BINARY-* -- multiplication function

• BINARY-+ -- addition function

• BINARY-APPEND -- concatenate two lists

• BOOLEANP -- recognizer for booleans

• 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

• 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

• CERTIFY-BOOK -- how to produce a certificate for a 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

• CHARACTERP -- recognizer for characters

• CHARACTERS -- characters in ACL2

• CODE-CHAR -- the character corresponding to a given numeric code

• COERCE -- coerce a character list to a string and a string to a list

• COMP-GCL -- compile some ACL2 functions leaving .c and .h files

• COMPILATION -- compiling ACL2 functions

• COMPLEX -- create an ACL2 number

• COMPLEX-RATIONALP -- recognizes complex rational numbers

• COMPLEX/COMPLEX-RATIONALP -- recognizer for complex numbers

• CONCATENATE -- concatenate lists or strings together

• COND -- conditional based on if-then-else

• CONJUGATE -- complex number conjugate

• CONS -- pair and list constructor

• CONSP -- recognizer for cons pairs

• CW -- print to the comment window

• DECLARE -- declarations

• DEFCONST -- define a constant

• DEFPKG -- define a new symbol package

• DEFUN -- define a function symbol

• 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

• E0-ORD-< -- the old ordering function for ACL2 ordinals

• E0-ORDINALP -- the old recognizer for ACL2 ordinals

• EIGHTH -- eighth member of the list

• ENDP -- recognizer for empty lists

• 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

• ER -- print an error message and ``cause an error''

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

• ERROR1 -- print an error message and cause a ``soft error''

• EVENP -- test whether an integer is even

• EXPLODE-NONNEGATIVE-INTEGER -- the list of characters in the radix-r form of a number

• EXPT -- exponential function

• FIFTH -- fifth member of the list

• 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

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

• FMT -- formatted printing

• FMT! -- :(str alist co-channel state evisc) => state

• FMT-TO-COMMENT-WINDOW -- print to the comment window

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

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

• FOURTH -- fourth member of the list

• HARD-ERROR -- print an error message and stop execution

• IDENTITY -- the identity function

• IF -- if-then-else function

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

• IFIX -- coerce to an integer

• ILLEGAL -- print an error message and stop execution

• IMAGPART -- imaginary part of a complex number

• IMPLIES -- logical implication

• IMPROPER-CONSP -- recognizer for improper (non-null-terminated) non-empty lists

• 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$ -- create a new symbol in a given package

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

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

• INTERSECTP-EQUAL -- test whether two lists intersect

• IO -- input/output facilities in ACL2

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

• 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

• 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

• LIST -- build a list

• LIST* -- build a list

• LISTP -- recognizer for (not necessarily proper) lists

• 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

• 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

• LOWER-CASE-P -- recognizer for lower case characters

• MAKE-CHARACTER-LIST -- coerce to a list of characters

• MAKE-LIST -- make a list of a given size

• MAKE-ORD -- a constructor for ordinals.

• MAX -- the larger of two numbers

• MBE -- attach code for execution

• MBT -- introduce a test not to be evaluated

• MEMBER -- membership predicate, using eql as test

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

• MEMBER-EQUAL -- membership predicate

• MIN -- the smaller of two numbers

• MINUSP -- test whether a number is negative

• MOD -- remainder using floor

• MUST-BE-EQUAL -- attach code for execution

• MUTUAL-RECURSION -- define some 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

• NATP -- a recognizer for the natural numbers

• NFIX -- coerce to a natural number

• NINTH -- ninth member of the list

• NO-DUPLICATESP -- check for duplicates in a list (using eql for equality)

• NO-DUPLICATESP-EQUAL -- check for duplicates in a list (using equal for equality)

• NONNEGATIVE-INTEGER-QUOTIENT -- natural number division function

• NOT -- logical negation

• 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

• 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

• ODDP -- test whether an integer is odd

• OR -- disjunction

• PAIRLIS -- See pairlis$

• PAIRLIS$ -- zipper together two lists

• PKG-WITNESS -- return a specific symbol in the indicated package

• PLUSP -- test whether a number is positive

• 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

• POSP -- a recognizer for the positive integers

• PPROGN -- evaluate a sequence of forms that return state

• PROG2$ -- execute two forms and return the value of the second one

• PROGN -- an abbreviation for er-progn

• PROOFS-CO -- the proofs character output channel

• PROPER-CONSP -- recognizer for proper (null-terminated) non-empty lists

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

• PUT-ASSOC-EQL -- 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

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

• RASSOC-EQ -- look up value in association list, using eq as test

• RASSOC-EQUAL -- look up value in association list, using equal as test

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

• RATIONALP -- recognizer for rational numbers (ratios and integers)

• 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

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

• 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-EQ -- remove all occurrences, testing using eq

• REMOVE-EQUAL -- remove all occurrences, testing using equal

• REMOVE1 -- remove first occurrences, testing using eql

• REMOVE1-EQ -- remove first occurrences, testing using eq

• REMOVE1-EQUAL -- remove first occurrences, testing using equal

• REST -- rest (cdr) of the list

• REVAPPEND -- concatentate the reverse of one list to another

• REVERSE -- reverse a list or string

• RFIX -- coerce to a rational number

• ROUND -- division returning an integer by rounding off

• SECOND -- second member of the list

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

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

• SET-DIFFERENCE-EQ -- elements of one list that are not elements of another

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

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

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

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

• SEVENTH -- seventh member of the list

• SIGNUM -- indicator for positive, negative, or zero

• SIXTH -- sixth member of the list

• 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-STRING-ALISTP -- recognizer for association lists with standard strings as keys

• 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

• 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

• SUBSTITUTE -- substitute into a string or a list, using eql as test

• 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

• SYS-CALL -- make a system call to the host operating system

• SYS-CALL-STATUS -- exit status from the preceding system call

• TAKE -- initial segment of a list

• TENTH -- tenth member of the list

• THE -- run-time type check

• THIRD -- third member of the list

• 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

• TYPE-SPEC -- type specifiers in declarations

• UNARY-- -- arithmetic negation function

• UNARY-/ -- reciprocal function

• UNION-EQ -- union of two lists of symbols

• UNION-EQUAL -- union of two lists

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

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

• 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