ACL2-BUILT-INS

Major Section:  PROGRAMMING

This documentation topic is a parent topic under which we include documentation for built-in functions, macros, and special forms that are typically used in programming. For others, including those typically used as top-level commands or those that create events (defun, defthm, and so on), documentation may be found as a subtopic of some other parent topic. We do not document some of the more obscure functions provided by ACL2 that do not correspond to functions of Common Lisp.

Some Related Topics

• * -- multiplication macro

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

• ABS -- the absolute value of a real number

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

• ACL2-NUMBER-LISTP -- recognizer for a true list of numbers

• ACL2-NUMBERP -- recognizer for numbers

• ACONS -- constructor for association lists

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

• 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 zero or more lists

• ASH -- arithmetic shift operation

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

• 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

• BINARY-* -- multiplication function

• BINARY-+ -- addition function

• BINARY-APPEND -- concatenate two lists

• BOOLE$ -- perform a bit-wise logical operation on 2 two's complement integers

• BOOLEANP -- recognizer for booleans

• BREAK$ -- cause an immediate Lisp break

• BREAKS -- Common Lisp breaks

• 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

• 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

• 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

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

• CLOSE-INPUT-CHANNEL -- See io.

• CLOSE-OUTPUT-CHANNEL -- See io.

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

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

• 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

• COUNT -- count the number of occurrences of an item in a string or true-list

• CPU-CORE-COUNT -- the number of cpu cores

• CW -- print to the comment window

• CW! -- print to the comment window

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

• 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

• EC-CALL -- execute a call in the ACL2 logic instead of raw Lisp

• 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

• F-GET-GLOBAL -- get the value of a global variable in state

• F-PUT-GLOBAL -- assign to a global variable in state

• 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

• FLET -- local binding of function symbols

• 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

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

• FOURTH -- fourth member of the list

• GET-OUTPUT-STREAM-STRING$ -- See io.

• GETENV$ -- read an environment variable

• GETPROP -- access fast property lists

• GOOD-ATOM-LISTP -- recognizer for a true list of ``good'' atoms

• 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

• INTERSECTION$ -- elements of one list that are not elements of another

• INTERSECTION-EQ -- See intersection$.

• INTERSECTION-EQUAL -- See intersection$.

• INTERSECTP -- test whether two lists intersect

• INTERSECTP-EQ -- See intersectp.

• INTERSECTP-EQUAL -- See intersectp.

• 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

• 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

• MBE1 -- attach code for execution

• MBT -- introduce a test not to be evaluated

• MEMBER -- membership predicate

• MEMBER-EQ -- See member.

• MEMBER-EQUAL -- See member.

• MIN -- the smaller of two numbers

• MINUSP -- test whether a number is negative

• MOD -- remainder using floor

• MOD-EXPT -- exponential function

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

• 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

• NAT-LISTP -- recognizer for a true list of natural numbers

• 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

• NO-DUPLICATESP-EQ -- See no-duplicatesp.

• NO-DUPLICATESP-EQUAL -- See no-duplicatesp.

• NON-EXEC -- mark code as non-executable

• 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

• OBSERVATION -- print an observation

• OBSERVATION-CW -- See observation.

• ODDP -- test whether an integer is odd

• OPEN-INPUT-CHANNEL -- See io.

• OPEN-INPUT-CHANNEL-P -- See io.

• OPEN-OUTPUT-CHANNEL -- See io.

• OPEN-OUTPUT-CHANNEL-P -- See io.

• 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

• PAIRLIS -- See pairlis$

• PAIRLIS$ -- zipper together two lists

• PEEK-CHAR$ -- See io.

• PKG-IMPORTS -- list of symbols imported into a given package

• 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

• POSITION-EQ -- See position.

• POSITION-EQUAL -- See position.

• POSP -- a recognizer for the positive integers

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

• PRINC$ -- print an atom

• PRINT-OBJECT$ -- See io.

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

• PROGN$ -- execute a sequence of forms and return the value of the last one

• PROOFS-CO -- the proofs character output channel

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

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

• 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

• 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/RATIONALP -- recognizer for rational numbers (including real number in ACL2(r))

• REALFIX -- coerce to a real number

• REALPART -- real part of a complex number

• REM -- remainder using truncate

• REMOVE -- remove all occurrences

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

• REMOVE1 -- remove first occurrences, testing using eql

• REMOVE1-EQ -- See remove1.

• REMOVE1-EQUAL -- See remove1.

• REST -- rest (cdr) of the list

• RETURN-LAST -- return the last argument, perhaps with side effects

• 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

• SEARCH -- search for a string or list in another string or list

• SECOND -- second member of the list

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

• SET-DIFFERENCE-EQ -- See set-difference$.

• SET-DIFFERENCE-EQUAL -- See set-difference$.

• SETENV$ -- set an environment variable

• 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

• STATE-GLOBAL-LET* -- bind state global variables

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

• 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

• TERM-ORDER -- the ordering relation on terms used by ACL2

• THE -- run-time type check

• THIRD -- third member of the list

• TIME$ -- time an evaluation

• 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

• UNARY-- -- arithmetic negation function

• UNARY-/ -- reciprocal function

• UNION$ -- elements of one list that are not elements of another

• UNION-EQ -- See union$.

• UNION-EQUAL -- See union$.

• 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

• WITH-LIVE-STATE -- allow a reference to state in raw Lisp

• WRITE-BYTE$ -- See io.

• XOR -- logical ``exclusive or''

• 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

See any documentation for Common Lisp for more details on many of these functions.