''Catch-all'' topic for built-in ACL2 functions

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`, `defmacro`, `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.

If you are already familiar with Common Lisp (or even some other Lisp variant), then you may find it helpful to start with the topic, introduction-to-programming-in-ACL2-for-those-who-know-lisp.

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

- Let
- Binding of lexically scoped (local) variables
- Declare
- Extra declarations that can occur in function definitions, let bindings, and so forth.
- Mbe
- Attach code for execution
- Apply$
- Apply a badged function or tame lambda to arguments
- Fmt
- Formatted printing
- Loop$
- Iteration with an analogue of the Common Lisp
loop macro - Return-last
- Return the last argument, perhaps with side effects
- Mv-let
- Calling multi-valued ACL2 functions
- Pseudo-termp
- A predicate for recognizing term-like s-expressions
- Defwarrant
- Issue a warrant for a function so
`apply$`can use it in proofs - Time$
- Time the evaluation of a given form
- Mv-nth
- The mv-nth element (zero-based) of a list
- Ec-call
- Execute a call in the ACL2 logic instead of raw Lisp
- Sys-call
- Make a system call to the host operating system
- Mbt
- Introduce a test into the logic that, however, evaluates to
t - Msg
- Construct a ``message'' suitable for the
~@ directive of`fmt` - Er
- Print an error message and ``cause an error''
- Value-triple
- Compute a value, optionally checking that it is not
nil - Comp
- Compile some ACL2 functions
- O-p
- A recognizer for the ordinals up to epsilon-0
- Member
- Membership predicate
- O<
- The well-founded less-than relation on ordinals up to
epsilon-0 - Cw
- Print to the comment window
- Or
- Disjunction
- Hons
(hons x y) returns a normed object equal to(cons x y) .- Cbd
- Connected book directory string
- Flet
- Local binding of function symbols
- Mv
- Returning a multiple value
- Defbadge
- Issue a badge for a function so
`apply$`can evaluate with it - Append
- concatenate zero or more lists
- *ACL2-exports*
- Symbols that are often imported into new packages to provide easy access to ACL2 functionality.
- Eql
- Test equality (of two numbers, symbols, or characters)
- Comment
- Variant of
`prog2$`to help debug evaluation failures during proofs - Posp
- A recognizer for the positive integers
- Natp
- A recognizer for the natural numbers
- Nth
- The nth element (zero-based) of a list
- Unsigned-byte-p
- Recognizer for natural numbers that fit in a specified bit width
- And
- Conjunction
- Len
- Length of a list
- List
- Build a list
- Time-tracker
- Display time spent during specified evaluation
- Term-order
- The ordering relation on terms used by ACL2
- True-listp
- Recognizer for proper (
nil -terminated) lists - Msgp
- Recognizer for a ``message''
- Booleanp
- Recognizer for booleans
- <
- Less-than
- If
- If-then-else function
- Pseudo-term-listp
- A predicate for recognizing lists of term-like s-expressions
- +
- Addition macro
- Not
- Logical negation
- Bitp
- A recognizer for the set of bits, {0,1}
- Equal
- True equality
- Cdr
- Returns the second element of a
`cons`pair, elsenil - Car
- Returns the first element of a non-empty list, else
nil - With-global-stobj
- Operate on a global single-threaded object
- String-listp
- Recognizer for a true list of strings
- Nat-listp
- Recognizer for a true list of natural numbers
- Implies
- Logical implication
- Iff
- Logical ``if and only if''
- Character-listp
- Recognizer for a true list of characters
- Alistp
- Recognizer for association lists
- The
The is a special form that can be used to optimize the execution efficiency of guard-verified ACL2 definitions, or (less frequently) to carry out a low-level run-time type checks. (Advanced)- Cons
- Pair and list constructor
- Symbol-listp
- Recognizer for a true list of symbols
- Quote
- Create a constant
- Integerp
- Recognizer for whole numbers
- Consp
- Recognizer for cons pairs
- True-list-listp
- Recognizer for true (proper) lists of true lists
- State-global-let*
- Bind state global variables
- Compress1
- Remove irrelevant pairs from a 1-dimensional array
- Symbolp
- Recognizer for symbols
- Stringp
- Recognizer for strings
- *common-lisp-symbols-from-main-lisp-package*
- Symbols that are often imported into new packages to provide easy access to Common Lisp functionality.
- Prog2$
- Execute two forms and return the value of the second one
- Characterp
- Recognizer for characters
- *
- Multiplication macro
- Macrolet
- Local binding of macro symbols
- Last-prover-steps
- The number of prover steps most recently taken
- Hons-acons
(hons-acons key val alist) is the main way to create or extend fast-alists.- Eq
- Equality of symbols
- Let*
- Binding of lexically scoped (local) variables
- With-guard-checking
- Suppress or enable guard-checking for a form
- With-local-stobj
- Locally bind a single-threaded object
- Length
- Length of a string or proper list
- @
- Get the value of a global variable in
`state` - Hard-error
- Print an error message and stop execution
- Search
- Search for a string or list in another string or list
- Zp
- Testing a ``natural'' against 0
- Intersection$
- Elements common to the given lists
- Aset1
- Set the elements of a 1-dimensional array
- -
- Macro for subtraction and negation
- Assign
- Assign to a global variable in
`state` - Symbol-name
- The name of a symbol (a string)
- Union$
- A list that contains exactly the elements of the given lists
- Set-gc-strategy
- Set the garbage collection strategy (CCL only)
- In-tau-intervalp
- Boolean membership in a tau interval
- Break-on-error
- Break when encountering a hard or soft error caused by ACL2
- Pand
- Parallel, Boolean version of
`and` - Cons-with-hint
- Alternative to
`cons`that tries to avoid consing when a suitablecons structure is provided as a hint. - Case-match
- Pattern matching or destructuring
- Fast-alist-fork
(fast-alist-fork alist ans) can be used to eliminate "shadowed pairs" from an alist or to copy fast-alists.- Sys-call+
- Make a system call to the host OS, returning status and output
- Signed-byte-p
- Recognizer for signed integers that fit in a specified bit width
- ACL2-count
- A commonly used measure for justifying recursion
- Remove-duplicates
- Remove duplicates from a string or a list
- With-serialize-character
- Control output mode for
print-object$ - Observation
- Print an observation
- Hons-resize
(hons-resize ...) can be used to manually adjust the sizes of the hash tables that govern which ACL2 Objects are considered normed.- Make-tau-interval
- Make a tau interval
- Logbitp
- The
i th bit of an integer - *standard-co*
- The ACL2 analogue of CLTL's
*standard-output* - Termp
- recognizer for the quotation of a term
- Position
- Position of an item in a string or a list
- Hons-acons!
(hons-acons! key val alist) is an alternative to`hons-acons`that produces normed, fast alists.- Assoc
- Look up key in association list
- Aref1
- Access the elements of a 1-dimensional array
- Read-run-time
- Read elapsed runtime
- Take
- Initial segment (first n elements) of a list
- Hons-wash
(hons-wash) is like`gc$`but can also garbage collect normed objects (CCL and GCL Only).- Symbol-package-name
- The name of the package of a symbol (a string)
- Expt
- Exponential function
- Coerce
- Coerce a character list to a string and a string to a list
- Intern
- Create a new symbol in a given package
- Update-nth
- Modify a list by putting the given value at the given position
- Standard-oi
- The standard object input ``channel''
- Non-exec
- Mark code as non-executable
- Standard-co
- The character output channel to which
`ld`prints - Get-internal-time
- Runtime vs. realtime in ACL2 timings
- Formula
- The formula of a name or rune
- Keywordp
- Recognizer for keywords
- Atom
- Recognizer for atoms
- Without-evisc
- Print output in full
- Good-bye
- Quit entirely out of Lisp
- Case
- Conditional based on if-then-else using
`eql` - With-local-state
- Locally bind state
- Spec-mv-let
- Modification of
`mv-let`supporting speculative and parallel execution - Intern-in-package-of-symbol
- Create a symbol with a given name
- Hons-clear
(hons-clear gc) is a drastic garbage collection mechanism that clears out the underlying Hons Space.- Binary-+
- Addition function
- Ash
- Arithmetic shift operation
- With-fast-alist
(with-fast-alist name form) causesname to be a fast alist for the execution ofform .- Set-difference$
- Elements of one list that are not elements of another
- Flush-compress
- Flush the under-the-hood array for the given name
- Rationalp
- Recognizer for rational numbers (ratios and integers)
- Symbol-alistp
- Recognizer for association lists with symbols as keys
- Por
- Parallel, Boolean version of
`or` - Rassoc
- Look up value in association list
- Remove-assoc
- Remove all pairs with a given key from an association list
- Pargs
- Parallel evaluation of arguments in a function call
- Hons-copy
(hons-copy x) returns a normed object that is equal to X.- Alphorder
- Total order on atoms
- =
- Test equality of two numbers
- Subsetp
- Test if every
`member`of one list is a`member`of the other - Logand
- Bitwise logical `and' of zero or more integers
- Remove1-assoc
- Remove the first pair with a given key from an association list
- No-duplicatesp
- Check for duplicates in a list
- Mv-list
- Converting multiple-value result to a single-value list
- Canonical-pathname
- The true absolute filename, with soft links resolved
- Aset2
- Set the elements of a 2-dimensional array
- <=
- Less-than-or-equal test
- Floor
- Division returning an integer by truncating toward negative infinity
- Serialize-read
- Read a serialized ACL2 object from a file
- Fmt-to-comment-window
- Print to the comment window
- F-put-global
- Assign to a global variable in
`state` - Compress2
- Remove irrelevant pairs from a 2-dimensional array
- Nthcdr
- Final segment of a list
- Concatenate
- Concatenate lists or strings together
- Random$
- Obtain a random value
- Nfix
- Coerce to a natural number
- Fast-alist-clean
(fast-alist-clean alist) can be used to eliminate "shadowed pairs" from a fast alist.- Remove
- Remove all occurrences
- Remove1
- Remove first occurrences, testing using
`eql` - Intersectp
- Test whether two lists intersect
- Assert$
- Cause a hard error if the given test is false
- Endp
- Recognizer for empty lists
- Put-assoc
- Modify an association list by associating a value with a key
- Princ$
- Print an atom
- Primitive
- Primitive functions built into ACL2 without definitions
- Standard-char-p
- Recognizer for standard characters
- True-list-fix
- Coerce to a true list
- Keyword-value-listp
- Recognizer for true lists whose even-position elements are keywords
- Illegal
- Print an error message and stop execution
- Hons-get
(hons-get key alist) is the efficient lookup operation for fast-alists.- With-output-lock
- Provides a mutual-exclusion mechanism for performing output in parallel
- Setenv$
- Set an environment variable
- Open-output-channel!
- When trust tags are needed to open output channels
- Fast-alist-free
(fast-alist-free alist) throws away the hash table associated with a fast alist.- Er-progn
- Perform a sequence of state-changing ``error triples''
- Cw-print-base-radix
- Print to the comment window in a given print-base
- Reverse
- Reverse a list or string
- Cond
- Conditional based on if-then-else
- Complex
- Create an ACL2 number
- Add-to-set
- Add a symbol to a list
- Truncate
- Division returning an integer by truncating toward 0
- Digit-char-p
- The number, if any, corresponding to a given character
- Code-char
- The character corresponding to a given numeric code
- Swap-stobjs
- Swap two congruent stobjs
- Set-print-case
- Control whether symbols are printed in upper case or in lower case
- Set-print-base
- Control radix in which numbers are printed
- Error1
- Print an error message and cause a ``soft error''
- Read-ACL2-oracle
- Pop the oracle field of the state
- Print-object$
- Print an object to an open object output channel
- Plet
- Parallel version of
`let` - Fmx-cw
(fmx-cw str &rest args) => state - Integer-length
- Number of bits in two's complement integer representation
- Zip
- Testing an ``integer'' against 0
- With-live-state
- Allow a reference to
state in raw Lisp - Hons-assoc-equal
(hons-assoc-equal key alist) is**not fast**; it serves as the logical definition for`hons-get`.- Extend-pathname
- Extend a relative pathname to an absolute pathname
- Logior
- Bitwise logical inclusive or of zero or more integers
- Char-code
- The numeric code for a given character
- With-guard-checking-event
- Suppress or enable guard-checking for an event form
- Term-listp
- recognizer for a list of quotations of terms and of clauses
- Print-object$+
- Print an object to an open output channel in a specified manner
- String
- coerce to a string
- In-package
- Select current package
- Unary--
- Arithmetic negation function
- Set-print-radix
- Control printing of the radix for numbers
- Resize-list
- List resizer in support of stobjs
- Pkg-witness
- Return a specific symbol in the indicated package
- Integer-listp
- Recognizer for a true list of integers
- Revappend
- Concatenate the reverse of one list to another
- Null
- Recognizer for the empty list
- Mod
- Remainder using
`floor` - Term-list-listp
- recognizer for a list of clauses
- Make-fast-alist
(make-fast-alist alist) creates a fast-alist from the input alist, returningalist itself or, in some cases, a new object equal to it.- Header
- Return the header of a 1- or 2-dimensional array
- Boole$
- Perform a bit-wise logical operation on 2 two's complement integers
- Subseq
- Subsequence of a string or list
- With-guard-checking-error-triple
- Suppress or enable guard-checking for a form
- /
- Macro for division and reciprocal
- Make-list
- Make a list of a given size
- Logxor
- Bitwise logical exclusive or of zero or more integers
- Strip-cars
- Collect up all first components of pairs in a list
- Set-fmt-hard-right-margin
- Set the right margin for formatted output
- Make-ord
- A constructor for ordinals.
- Fast-alist-free-on-exit
- Free a fast alist after the completion of some form.
- F-get-global
- Get the value of a global variable in
`state` - Aref2
- Access the elements of a 2-dimensional array
- Lognot
- Bitwise not of a two's complement number
- Must-be-equal
- Attach code for execution
- Integer-range-p
- Recognizer for integers between two bounds.
- Getenv$
- Read an environment variable
- Binary-append
- concatenate two lists
- Ifix
- Coerce to an integer
- Er-hard
- Print an error message and ``cause a hard error''
- Eqlablep
- The guard for the function
`eql` - Cpu-core-count
- The number of cpu cores
- ACL2-numberp
- Recognizer for numbers
- Butlast
- All but a final segment of a list
- Pairlis$
- Zipper together two lists
- Mod-expt
- Exponential function
- Hons-equal
(hons-equal x y) is a recursive equality check that optimizes when parts of its arguments are normed.- Gc$
- Invoke the garbage collector
- Boolean-listp
- Recognizer for a true list of booleans
- Substitute
- Substitute into a string or a list, using
`eql`as test - Ceiling
- Division returning an integer by truncating toward positive infinity
- With-stolen-alist
(with-stolen-alist name form) ensures thatname is a fast alist at the start of the execution ofform . At the end of execution, it ensures thatname is a fast alist if and only if it was originally. That is, ifname 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 ofform , that table is restored. Note that any extended table created from the original fast alist duringform must be manually freed.- Mv?-let
- Calling possibly multi-valued ACL2 functions
- Round
- Division returning an integer by rounding off
- Count
- Count the number of occurrences of an item in a string or true-list
- Char
- The nth element (zero-based) of a string
- Sys-call-status
- Exit status from the preceding system call
- Progn$
- Execute a sequence of forms and return the value of the last one
- Pprogn
- Evaluate a sequence of forms that return state
- Lexorder
- Total order on ACL2 objects
- Hons-summary
(hons-summary) prints basic information about the sizes of the tables in the current Hons Space.- Break$
- Cause an immediate Lisp break
- Assert*
- Create a guard proof obligation that given test holds
- Char-upcase
- Turn lower-case characters into upper-case characters
- Char-downcase
- Turn upper-case characters into lower-case characters
- Strip-cdrs
- Collect up all second components of pairs in a list
- Serialize-write
- Write an ACL2 object into a file
- Proofs-co
- The proofs character output channel
- Keyword-listp
- Recognizer for true lists of keywords
- String-downcase
- In a given string, turn upper-case characters into lower-case
- Logeqv
- Bitwise logical equivalence of zero or more integers
- List*
- Build a list
- Maximum-length
- Return the
:maximum-length from the header of an array - Explode-nonnegative-integer
- The list of characters in the radix-r form of a number
- Eqlable-listp
- Recognizer for a true list of objects each suitable for
`eql` - Dimensions
- Return the
:dimensions from the header of a 1- or 2-dimensional array - Default
- Return the
:default from the header of a 1- or 2-dimensional array - Arity
- number of arguments of a function symbol
- Sublis
- Substitute an alist into a tree
- String-upcase
- In a given string, turn lower-case characters into upper-case
- Max
- The larger of two numbers
- Evenp
- Test whether an integer is even
- Explode-atom
- Convert any atom into a character-listp that contains its printed representation, rendering numbers in your choice of print base.
- Change
- Mutator macro for defrec structures.
- Zerop
- Test an acl2-number against 0
- String<
- Less-than test for strings
- Last
- The last
`cons`(not element) of a list - Abs
- The absolute value of a real number
- Set-print-base-radix
- Control radix in which numbers are printed and printing of the radix
- Nonnegative-integer-quotient
- Natural number division function
- Intern$
- Create a new symbol in a given package
- Getprop
- Access fast property lists
- Binary-*
- Multiplication function
- Aset1-trusted
- Set the elements of a 1-dimensional array without invariant-risk
- *standard-oi*
- An ACL2 object-based analogue of CLTL's
*standard-input* - Symbol<
- Less-than test for symbols
- String-append
- concatenate two strings
- Print-base-p
- Recognizer for print bases that are understood by functions such as explode-nonnegative-integer and explode-atom.
- Mv?
- Return one or more values
- Logic-fns-list-listp
- Recognizer for when a given list of lists of terms calls only
: `logic`-mode function symbols - Fix
- Coerce to a number
- Fast-alist-fork!
(fast-alist-fork! alist ans) is an alternative to`fast-alist-fork`that produces a normed result.- Er-hard?
- Print an error message and ``cause a hard error''
- Allocate-fixnum-range
- Set aside fixnums in GCL
- String-equal
- String equality without regard to case
- 1+
- Increment by 1
- Sys-call*
- Make a system call to the host OS, returning a status
- Pos-listp
- Recognizer for a true list of positive integers
- Mbt*
- Introduce a guard proof obligation
- Hons-wash!
- A version of
`hons-wash`for parallel execution - Hons-clear!
- A version of
`hons-clear`for parallel execution - Upper-case-p
- Recognizer for upper case characters
- Signum
- Indicator for positive, negative, or zero
- Rem
- Remainder using
`truncate` - Lower-case-p
- Recognizer for lower case characters
- Char-equal
- Character equality without regard to case
- Alpha-char-p
- Recognizer for alphabetic characters
- Real/rationalp
- Recognizer for rational numbers (including real number in ACL2(r))
- Rational-listp
- Recognizer for a true list of rational numbers
- O-first-coeff
- Returns the first coefficient of an ordinal
- Logic-fnsp
- Recognizer for when a given term calls only
: `logic`-mode function symbols - Logic-fns-listp
- Recognizer for when a given list of terms calls only
: `logic`-mode function symbols - 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`.- Gc-strategy
- The garbage collection strategy
- Fast-alist-summary
(fast-alist-summary) prints some basic statistics about any current fast alists.- String>=
- Less-than-or-equal test for strings
- String<=
- Less-than-or-equal test for strings
- Acons
- Constructor for association lists
- Rfix
- Coerce to a rational number
- O-first-expt
- The first exponent of an ordinal
- Fast-alist-clean!
(fast-alist-clean! alist) is an alternative to`fast-alist-clean`that produces a normed result.- >=
- Greater-than-or-equal test
- >
- Greater-than test
- Subst
- A single substitution into a tree
- Logcount
- Number of ``on'' bits in a two's complement number
- Getpropc
- Access fast property lists
- Evens
- The even-indexed members of a list
- Er-soft
- Print an error message and ``cause a soft error''
- Digit-to-char
- Map a digit to a character
- Comp-gcl
- Compile some ACL2 functions leaving .c and .h files
- Atom-listp
- Recognizer for a true list of atoms
- Arities-okp
- check the arities of given function symbols
- ACL2-number-listp
- Recognizer for a true list of numbers
- /=
- Test inequality of two numbers
- Cadr
`car`of the`cdr`- *standard-ci*
- An ACL2 character-based analogue of CLTL's
*standard-input* - Unary-/
- Reciprocal function
- The-true-list
- Coerce an expected true list to a true list
- O-rst
- Returns the rest of an infinite ordinal
- Fast-alist-len
(fast-alist-len alist) counts the number of unique keys in a fast alist.- Complex/complex-rationalp
- Recognizer for complex numbers
- Array2p
- Recognize a 2-dimensional array
- Array1p
- Recognize a 1-dimensional array
- Logtest
- Test if two integers share a `1' bit
- Logandc1
- Bitwise logical `and' of two ints, complementing the first
- Char<
- Less-than test for characters
- Putprop
- Update fast property lists
- Get-real-time
- Read elapsed real time
- Eqlable-alistp
- Recognizer for a true list of pairs whose
`car`s are suitable for`eql` - Count-keys
- Count the number of keys in association list
- Assoc-string-equal
- Look up key, a string, in association list
- Logorc1
- Bitwise logical inclusive or of two ints, complementing the first
- Logandc2
- Bitwise logical `and' of two ints, complementing the second
- 1-
- Decrement by 1
- Standard-string-alistp
- Recognizer for association lists with standard strings as keys
- Packn
- Build a symbol from a list
- Logic-termp
- Recognizer for terms that call only
: `logic`-mode function symbols - Logic-term-list-listp
- Recognizer for lists of lists of terms that call only
: `logic`-mode function symbols - Fmt!
(fmt! str alist co-channel state evisc) => state - Fms
(fms str alist co-channel state evisc) => state - Cw!
- Print readably to the comment window
- Assoc-keyword
- Look up key in a
`keyword-value-listp` - String>
- Greater-than test for strings
- Numerator
- Dividend of a ratio in lowest terms
- Logorc2
- Bitwise logical inclusive or of two ints, complementing the second
- Listp
- Recognizer for (not necessarily proper) lists
- Denominator
- Divisor of a ratio in lowest terms
- Char>=
- Greater-than-or-equal test for characters
- The-number
- Coerce an expected number to a number
- Realfix
- Coerce to a real number
- Odds
- The odd-indexed members of a list
- Makunbound-global
- Remove the value assigned to a global variable in
`state` - Make-character-list
- coerce to a list of characters
- Make
- Constructor macro for defrec structures.
- Get-cpu-time
- Read elapsed cpu time
- Fmt-to-comment-window!
- Print readably to the comment window
- Fms!
(fms! str alist co-channel state evisc) => state - F-boundp-global
- Check whether a global variable in
`state`has a value - Complex-rationalp
- Recognizes complex rational numbers
- Alist-to-doublets
- Convert an alist to a list of two-element lists
- Access
- Accessor macro for defrec structures.
- Min
- The smaller of two numbers
- Lognor
- Bitwise logical `nor' of two integers
- Identity
- The identity function
- Char>
- Greater-than test for characters
- Char<=
- Less-than-or-equal test for characters
- Zpf
- Testing a nonnegative fixnum against 0
- Standard-char-listp
- Recognizer for a true list of standard characters
- O-finp
- Recognizes if an ordinal is finite
- Number-subtrees
(number-subtrees x) returns the number of distinct subtrees of X, in the sense of`equal`- Logic-term-listp
- Recognizer for lists of terms that call only
: `logic`-mode function symbols - Last-cdr
- The last
`cdr`of a list - Fmt1!
(fmt1! str alist col channel state evisc) => (mv col state) - Fmt-to-comment-window!+
- Print readably and uninhibited to the comment window
- Character-alistp
- Recognizer for association lists with characters as keys
- Oddp
- Test whether an integer is odd
- Minusp
- Test whether a number is negative
- Lognand
- Bitwise logical `nand' of two integers
- Imagpart
- Imaginary part of a complex number
- Conjugate
- Complex number conjugate
- Xor
- Logical ``exclusive or''
- Update-nth-array
- Update a stobj array
- Unquote
- Obtain the object being quoted
- Packn-pos
- Build a symbol in a specified package from a list
- Maybe-flush-and-compress1
- Compress a one-dimensional array only if necessary
- Kwote
- Quote an arbitrary object
- Int=
- Test equality of two integers
- Fmt1
(fmt1 str alist col co-channel state evisc) => (mv col state) - Fmt-to-comment-window+
- Print uninhibited to the comment window
- Cw-print-base-radix!
- Print to the comment window in a given print-base
- Alist-keys-subsetp
- Check that all keys of the alist belong to a given set
- Realpart
- Real part of a complex number
- Plusp
- Test whether a number is positive
- First
- First member of the list
- Symbol-name-lst
- Lift
`symbol-name`to lists - R-symbol-alistp
- Recognizer for association lists with symbols as values
- R-eqlable-alistp
- Recognizer for a true list of pairs whose
`cdr`s are suitable for`eql` - Cw!+
- Print readably and uninhibited to the comment window
- Cons-subtrees
- Build a fast alist whose keys are the subtrees of X
- Cons-count-bounded
- Count the number of conses (up to a limit)
- Cddr
`cdr`of the`cdr`- Caar
`car`of the`car`- Proper-consp
- Recognizer for proper (
nil -terminated) non-empty lists - Kwote-lst
- Quote an arbitrary true list of objects
- Improper-consp
- Recognizer for improper (non-
nil -terminated) non-empty lists - Fmx
(fmx str &rest args) => state - Cw+
- Print uninhibited to the comment window
- Rest
- Rest (
`cdr`) of the list - Standard-char-p+
- Recognizer for standard characters whose guard is
t - Mbe1
- Attach code for execution
- Caddr
`car`of the`cddr`- Pairlis-x2
- Cons each element of a list with a given element
- Pairlis-x1
- Cons a given element to each member of a list
- O>=
- The greater-than-or-equal relation for the ordinals
- O<=
- The less-than-or-equal relation for the ordinals
- O-infp
- Recognizes if an ordinal is infinite
- Merge-sort-lexorder
- Sort a list
- Fix-true-list
- Coerce to a true list
- Cdddr
`cdr`of the`cddr`- Set-fmt-soft-right-margin
- Set the soft right margin for formatted output
- Real-listp
- ACL2(r) recognizer for a true list of real numbers
- O>
- The greater-than relation for the ordinals
- Cddar
`cdr`of the`cdar`- Cdar
`cdr`of the`car`- Cdadr
`cdr`of the`cadr`- Cdaar
`cdr`of the`caar`- Cadar
`car`of the`cdar`- Caadr
`car`of the`cadr`- Caaar
`car`of the`caar`- Cadddr
`car`of the`cdddr`- Caddar
`car`of the`cddar`- Third
- Third member of the list
- Tenth
- Tenth member of the list
- Sixth
- Sixth member of the list
- Seventh
- Seventh member of the list
- Second
- Second member of the list
- Ninth
- Ninth member of the list
- Fourth
- Fourth member of the list
- Fifth
- Fifth member of the list
- Eighth
- Eighth member of the list
- Cddddr
`cdr`of the`cdddr`- Cdddar
`cdr`of the`cddar`- Cddadr
`cdr`of the`cdadr`- Cddaar
`cdr`of the`cdaar`- Cdaddr
`cdr`of the`caddr`- Cdadar
`cdr`of the`cadar`- Cdaadr
`cdr`of the`caadr`- Cdaaar
`cdr`of the`caaar`- Cadadr
`car`of the`cdadr`- Cadaar
`car`of the`cdaar`- Caaddr
`car`of the`caddr`- Caadar
`car`of the`cadar`- Caaadr
`car`of the`caadr`- Caaaar
`car`of the`caaar`- Hons-shrink-alist!
- Deprecated feature
- Hons-shrink-alist
- Deprecated feature
- Flush-hons-get-hash-table-link
- Deprecated feature
- Delete-assoc
- Deprecated version of remove1-assoc