''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
- Ec-call
- Execute a call in the ACL2 logic instead of raw Lisp
- Sys-call
- Make a system call to the host operating system
- Msg
- Construct a ``message'' suitable for the
~@ directive of`fmt` - Mbt
- Introduce a test into the logic that, however, evaluates to
t - Mv-nth
- The mv-nth element (zero-based) of a list
- 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
- Er
- Print an error message and ``cause an error''
- Or
- Disjunction
- Hons
(hons x y) returns a normed object equal to(cons x y) .- Flet
- Local binding of function symbols
- Mv
- Returning a multiple value
- Append
- concatenate zero or more lists
- Defbadge
- Issue a badge for a function so
`apply$`can evaluate with it - Cbd
- Connected book directory string
- *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)
- Natp
- A recognizer for the natural numbers
- Comment
- Variant of
`prog2$`to help debug evaluation failures during proofs - Unsigned-byte-p
- Recognizer for natural numbers that fit in a specified bit width
- Posp
- A recognizer for the positive integers
- Nth
- The nth element (zero-based) of a list
- And
- Conjunction
- List
- Build a list
- Len
- Length of 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
- 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
- Symbol-listp
- Recognizer for a true list of symbols
- 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
- 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
- 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
- <
- Less-than
- *
- Multiplication macro
- Macrolet
- Local binding of macro symbols
- Characterp
- Recognizer for characters
- 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
- With-guard-checking
- Suppress or enable guard-checking for a form
- Let*
- Binding of lexically scoped (local) variables
- With-local-stobj
- Locally bind a single-threaded object
- Length
- Length of a string or proper list
- Hard-error
- Print an error message and stop execution
- Search
- Search for a string or list in another string or list
- @
- Get the value of a global variable in
`state` - Zp
- Testing a ``natural'' against 0
- State-global-let*
- Bind state global variables
- Aset1
- Set the elements of a 1-dimensional array
- Intersection$
- Elements common to the given lists
- -
- Macro for subtraction and negation
- Assign
- Assign to a global variable in
`state` - 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
- 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
- Symbol-name
- The name of a symbol (a string)
- 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
- Remove-duplicates
- Remove duplicates from a string or a list
- With-serialize-character
- Control output mode for
print-object$ - Hons-resize
(hons-resize ...) can be used to manually adjust the sizes of the hash tables that govern which ACL2 Objects are considered normed.- Observation
- Print an observation
- Make-tau-interval
- Make a tau interval
- ACL2-count
- A commonly used measure for justifying recursion
- Logbitp
- The
i th bit of an integer - Position
- Position of an item in a string or a list
- Termp
- recognizer for the quotation of a term
- *standard-co*
- The ACL2 analogue of CLTL's
*standard-output* - Hons-acons!
(hons-acons! key val alist) is an alternative to`hons-acons`that produces normed, fast alists.- Aref1
- Access the elements of a 1-dimensional array
- Assoc
- Look up key in association list
- Read-run-time
- Read elapsed runtime
- Hons-wash
(hons-wash) is like`gc$`but can also garbage collect normed objects (CCL and GCL Only).- Break-on-error
- Break when encountering a hard or soft error caused by ACL2
- Expt
- Exponential function
- Take
- Initial segment (first n elements) of a list
- Symbol-package-name
- The name of the package of a symbol (a string)
- Coerce
- Coerce a character list to a string and a string to a list
- Intern
- Create a new symbol in a given package
- Atom
- Recognizer for atoms
- Standard-oi
- The standard object input ``channel''
- Non-exec
- Mark code as non-executable
- Update-nth
- Modify a list by putting the given value at the given position
- Get-internal-time
- Runtime vs. realtime in ACL2 timings
- Formula
- The formula of a name or rune
- Keywordp
- Recognizer for keywords
- Without-evisc
- Print output in full
- Standard-co
- The character output channel to which
`ld`prints - 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
- Logand
- Bitwise logical `and' of zero or more integers
- 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
- <=
- Less-than-or-equal test
- Subsetp
- Test if every
`member`of one list is a`member`of the other - 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
- Aset2
- Set the elements of a 2-dimensional array
- Floor
- Division returning an integer by truncating toward negative infinity
- Concatenate
- Concatenate lists or strings together
- Serialize-read
- Read a serialized ACL2 object from a file
- Random$
- Obtain a random value
- 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
- Canonical-pathname
- The true absolute filename, with soft links resolved
- Primitive
- Primitive functions built into ACL2 without definitions
- 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
- Nthcdr
- Final segment of a list
- 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
- 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
- Digit-char-p
- The number, if any, corresponding to a given character
- Cond
- Conditional based on if-then-else
- With-output-lock
- Provides a mutual-exclusion mechanism for performing output in parallel
- Princ$
- Print an atom
- 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
- Truncate
- Division returning an integer by truncating toward 0
- Reverse
- Reverse a list or string
- Complex
- Create an ACL2 number
- Add-to-set
- Add a symbol to a list
- 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
- Code-char
- The character corresponding to a given numeric code
- Setenv$
- Set an environment variable
- Print-object$
- Print an object to an open object output channel
- Plet
- Parallel version of
`let` - Hons-get
(hons-get key alist) is the efficient lookup operation for fast-alists.- Fmx-cw
(fmx-cw str &rest args) => state - Error1
- Print an error message and cause a ``soft error''
- 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 - Logior
- Bitwise logical inclusive or of zero or more integers
- 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
- Hons-assoc-equal
(hons-assoc-equal key alist) is**not fast**; it serves as the logical definition for`hons-get`.- String
- coerce to a string
- Char-code
- The numeric code for a given character
- 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
- Boole$
- Perform a bit-wise logical operation on 2 two's complement integers
- /
- Macro for division and reciprocal
- Revappend
- Concatenate the reverse of one list to another
- Mod
- Remainder using
`floor` - In-package
- Select current package
- Term-list-listp
- recognizer for a list of clauses
- Read-ACL2-oracle
- Pop the oracle field of the state
- 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
- Extend-pathname
- Extend a relative pathname to an absolute pathname
- Subseq
- Subsequence of a string or list
- Null
- Recognizer for the empty list
- With-guard-checking-error-triple
- Suppress or enable guard-checking for a form
- 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
- Make-ord
- A constructor for ordinals.
- Fast-alist-free-on-exit
- Free a fast alist after the completion of some form.
- 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
- F-get-global
- Get the value of a global variable in
`state` - 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
- Ceiling
- Division returning an integer by truncating toward positive infinity
- 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
- Substitute
- Substitute into a string or a list, using
`eql`as test - Round
- Division returning an integer by rounding off
- 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
- Count
- Count the number of occurrences of an item in a string or true-list
- Char-downcase
- Turn upper-case characters into lower-case characters
- Char
- The nth element (zero-based) of a string
- Sys-call-status
- Exit status from the preceding system call
- Set-fmt-hard-right-margin
- Set the right margin for formatted output
- 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.- Boolean-listp
- Recognizer for a true list of booleans
- Assert*
- Create a guard proof obligation that given test holds
- List*
- Build a list
- Char-upcase
- Turn lower-case characters into upper-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
- Progn$
- Execute a sequence of forms and return the value of the last one
- Keyword-listp
- Recognizer for true lists of keywords
- Sublis
- Substitute an alist into a tree
- String-downcase
- In a given string, turn upper-case characters into lower-case
- Logeqv
- Bitwise logical equivalence of zero or more integers
- 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
- String-upcase
- In a given string, turn lower-case characters into upper-case
- Max
- The larger of two numbers
- Last
- The last
`cons`(not element) of a list - Evenp
- Test whether an integer is even
- Nonnegative-integer-quotient
- Natural number division function
- Change
- Mutator macro for defrec structures.
- Binary-append
- concatenate two lists
- Zerop
- Test an acl2-number against 0
- String<
- Less-than test for strings
- Abs
- The absolute value of a real number
- Set-print-base-radix
- Control radix in which numbers are printed and printing of the radix
- Intern$
- Create a new symbol in a given package
- Getprop
- Access fast property lists
- Explode-atom
- Convert any atom into a character-listp that contains its printed representation, rendering numbers in your choice of print base.
- Binary-*
- Multiplication function
- Aset1-trusted
- Set the elements of a 1-dimensional array without invariant-risk
- String-equal
- String equality without regard to case
- 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
- Rem
- Remainder using
`truncate` - Alpha-char-p
- Recognizer for alphabetic characters
- 1+
- Increment by 1
- *standard-oi*
- An ACL2 object-based analogue of CLTL's
*standard-input* - 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 - Break$
- Cause an immediate Lisp break
- Upper-case-p
- Recognizer for upper case characters
- String>=
- Less-than-or-equal test for strings
- String<=
- Less-than-or-equal test for strings
- Signum
- Indicator for positive, negative, or zero
- Lower-case-p
- Recognizer for lower case characters
- Char-equal
- Character equality without regard to case
- 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.- Acons
- Constructor for association lists
- Rfix
- Coerce to a rational number
- O-first-expt
- The first exponent of an ordinal
- Getpropc
- Access fast property lists
- Fast-alist-clean!
(fast-alist-clean! alist) is an alternative to`fast-alist-clean`that produces a normed result.- Digit-to-char
- Map a digit to a character
- >=
- 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
- Evens
- The even-indexed members of a list
- 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.- Er-soft
- Print an error message and ``cause a soft error''
- 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
- Good-atom-listp
- Recognizer for a true list of ``good'' atoms
- 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 - Get-cpu-time
- Read elapsed cpu time
- 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.
- 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
- Update-nth-array
- Update a stobj array
- 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''
- 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`- Standard-char-p+
- Recognizer for standard characters whose guard is
t - 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
- 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
- Rest
- Rest (
`cdr`) of the 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