''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
- Mv-let
- Calling multi-valued ACL2 functions
- Return-last
- Return the last argument, perhaps with side effects
- Pseudo-termp
- A predicate for recognizing term-like s-expressions
- Loop$
- Iteration with an analogue of the Common Lisp
loop macro - Time$
- Time an evaluation
- Ec-call
- Execute a call in the ACL2 logic instead of raw Lisp
- Defwarrant
- Issue a warrant for a function so
`apply$`can use it in proofs - Sys-call
- Make a system call to the host operating system
- Msg
- Construct a ``message'' suitable for the
~@ directive of`fmt` - Comp
- Compile some ACL2 functions
- Value-triple
- Compute a value, optionally checking that it is not
nil - O-p
- A recognizer for the ordinals up to epsilon-0
- Cbd
- Connected book directory string
- Member
- Membership predicate
- Mbt
- Introduce a test into the logic that, however, evaluates to
t - 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) .- Mv
- Returning a multiple value
- 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)
- Natp
- A recognizer for the natural numbers
- Er
- Print an error message and ``cause an error''
- Defbadge
- Issue a badge for a function so
`apply$`can evaluate with it - Comment
- Variant of
`prog2$`to help debug evaluation failures during proofs - Posp
- A recognizer for the positive integers
- Nth
- The nth element (zero-based) of a list
- And
- Conjunction
- Flet
- Local binding of function symbols
- Len
- Length of a list
- Term-order
- The ordering relation on terms used by ACL2
- Mv-nth
- The mv-nth element (zero-based) of a list
- True-listp
- Recognizer for proper (
nil -terminated) lists - Msgp
- Recognizer for a ``message''
- Booleanp
- Recognizer for booleans
- If
- If-then-else function
- Time-tracker
- Display time spent during specified evaluation
- Pseudo-term-listp
- A predicate for recognizing lists of term-like s-expressions
- +
- Addition macro
- Not
- Logical negation
- Unsigned-byte-p
- Recognizer for natural numbers that fit in a specified bit width
- 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 - 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
- Compress1
- Remove irrelevant pairs from a 1-dimensional array
- Symbolp
- Recognizer for symbols
- Stringp
- Recognizer for strings
- True-list-listp
- Recognizer for true (proper) lists of true lists
- *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
- List
- Build a list
- Hons-acons
(hons-acons key val alist) is the main way to create or extend fast-alists.- <
- Less-than
- Characterp
- Recognizer for characters
- Eq
- Equality of symbols
- *
- Multiplication macro
- 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
- Let*
- Binding of lexically scoped (local) variables
- Search
- Search for a string or list in another string or list
- @
- Get the value of a global variable in
`state` - Hard-error
- Print an error message and stop execution
- Aset1
- Set the elements of a 1-dimensional array
- Intersection$
- Elements common to the given lists
- State-global-let*
- Bind state global variables
- 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. - -
- Macro for subtraction and negation
- Zp
- Testing a ``natural'' against 0
- Fast-alist-fork
(fast-alist-fork alist ans) can be used to eliminate "shadowed pairs" from an alist or to copy fast-alists.- Case-match
- Pattern matching or destructuring
- Remove-duplicates
- Remove duplicates from a string or a list
- Position
- Position of an item in a string or a list
- 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
- 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
- With-serialize-character
- Control output mode for
print-object$ - ACL2-count
- A commonly used measure for justifying recursion
- Termp
- recognizer for the quotation of a term
- Logbitp
- The
i th bit of an integer - *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
- Symbol-name
- The name of a symbol (a string)
- Get-internal-time
- Runtime vs. realtime in ACL2 timings
- Assoc
- Look up key in association list
- 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
- Take
- Initial segment (first n elements) of a list
- Coerce
- Coerce a character list to a string and a string to a list
- Symbol-package-name
- The name of the package of a symbol (a string)
- Intern
- Create a new symbol in a given package
- Non-exec
- Mark code as non-executable
- Expt
- Exponential function
- Update-nth
- Modify a list by putting the given value at the given position
- Standard-oi
- The standard object input ``channel''
- Formula
- The formula of a name or rune
- Atom
- Recognizer for atoms
- Without-evisc
- Print output in full
- Last-prover-steps
- The number of prover steps most recently taken
- Good-bye
- Quit entirely out of Lisp
- 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
- Keywordp
- Recognizer for keywords
- Ash
- Arithmetic shift operation
- With-fast-alist
(with-fast-alist name form) causesname to be a fast alist for the execution ofform .- Standard-co
- The character output channel to which
`ld`prints - Set-difference$
- Elements of one list that are not elements of another
- Flush-compress
- Flush the under-the-hood array for the given name
- 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
- =
- Test equality of two numbers
- Rationalp
- Recognizer for rational numbers (ratios and 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
- 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
- Random$
- Obtain a random value
- No-duplicatesp
- Check for duplicates in a list
- Aset2
- Set the elements of a 2-dimensional array
- Logand
- Bitwise logical `and' of zero or more integers
- Serialize-read
- Read a serialized ACL2 object from a file
- Mv-list
- Converting multiple-value result to a single-value list
- 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
- Floor
- Division returning an integer by truncating toward negative infinity
- Concatenate
- Concatenate lists or strings together
- Primitive
- Primitive functions built into ACL2 without definitions
- Fast-alist-clean
(fast-alist-clean alist) can be used to eliminate "shadowed pairs" from a fast alist.- Canonical-pathname
- The true absolute filename, with soft links resolved
- Remove
- Remove all occurrences
- Nthcdr
- Final segment of a list
- Symbol-alistp
- Recognizer for association lists with symbols as keys
- Remove1
- Remove first occurrences, testing using
`eql` - Nfix
- Coerce to a natural number
- Intersectp
- Test whether two lists intersect
- Assert$
- Cause a hard error if the given test is false
- Put-assoc
- Modify an association list by associating a value with a key
- Keyword-value-listp
- Recognizer for true lists whose even-position elements are keywords
- <=
- Less-than-or-equal test
- Standard-char-p
- Recognizer for standard characters
- Digit-char-p
- The number, if any, corresponding to a given character
- With-output-lock
- Provides a mutual-exclusion mechanism for performing output in parallel
- Open-output-channel!
- When trust tags are needed to open output channels
- Illegal
- Print an error message and stop execution
- 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
- Complex
- Create an ACL2 number
- Princ$
- Print an atom
- 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
- Truncate
- Division returning an integer by truncating toward 0
- Reverse
- Reverse a list or string
- Cond
- Conditional based on if-then-else
- Code-char
- The character corresponding to a given numeric code
- Setenv$
- Set an environment variable
- Print-object$
- Print an an object to an open 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 - 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
- Endp
- Recognizer for empty lists
- 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 an object to an open output channel in a specified manner
- 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
- Integer-listp
- Recognizer for a true list of integers
- Hons-assoc-equal
(hons-assoc-equal key alist) is**not fast**; it serves as the logical definition for`hons-get`.- Boole$
- Perform a bit-wise logical operation on 2 two's complement integers
- String
- coerce to a string
- Case
- Conditional based on if-then-else using
`eql` - Term-list-listp
- recognizer for a list of clauses
- Read-ACL2-oracle
- Pop the oracle field of the state
- Pkg-witness
- Return a specific symbol in the indicated package
- 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
- /
- Macro for division and reciprocal
- Subseq
- Subsequence of a string or list
- Null
- Recognizer for the empty list
- In-package
- Select current package
- With-guard-checking-error-triple
- Suppress or enable guard-checking for a form
- Revappend
- Concatenate the reverse of one list to another
- Make-list
- Make a list of a given size
- Logxor
- Bitwise logical exclusive or of zero or more integers
- 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
- Strip-cars
- Collect up all first components of pairs in a list
- Must-be-equal
- Attach code for execution
- Integer-range-p
- Recognizer for integers between two bounds.
- Getenv$
- Read an environment variable
- Error1
- Print an error message and cause a ``soft error''
- Mod
- Remainder using
`floor` - Eqlablep
- The guard for the function
`eql` - Cpu-core-count
- The number of cpu cores
- Ceiling
- Division returning an integer by truncating toward positive infinity
- Butlast
- All but a final segment of a list
- Sys-call-status
- Exit status from the preceding system call
- Read-run-time
- Read elapsed runtime
- Mod-expt
- Exponential function
- Ifix
- Coerce to an integer
- 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
- F-get-global
- Get the value of a global variable in
`state` - 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.- Pairlis$
- Zipper together two lists
- Mv?-let
- Calling possibly multi-valued ACL2 functions
- ACL2-numberp
- Recognizer for numbers
- Lognot
- Bitwise not of a two's complement number
- 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
- 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
- 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
- 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
- Proofs-co
- The proofs character output channel
- 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 - String-upcase
- In a given string, turn lower-case characters into upper-case
- Nonnegative-integer-quotient
- Natural number division function
- Change
- Mutator macro for defrec structures.
- Binary-append
- concatenate two lists
- Arity
- number of arguments of a function symbol
- Zerop
- Test an acl2-number against 0
- String<
- Less-than test for strings
- Max
- The larger of two numbers
- 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.
- Aset1-trusted
- Set the elements of a 1-dimensional array without invariant-risk
- List*
- Build a list
- Evenp
- Test whether an integer is even
- 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 - Fast-alist-fork!
(fast-alist-fork! alist ans) is an alternative to`fast-alist-fork`that produces a normed result.- Binary-*
- Multiplication function
- Allocate-fixnum-range
- Set aside fixnums in GCL
- String-equal
- String equality without regard to case
- Last
- The last
`cons`(not element) of a list - 1+
- Increment by 1
- *standard-oi*
- An ACL2 object-based analogue of CLTL's
*standard-input* - 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
- 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
- Sys-call*
- Make a system call to the host OS, returning a status
- 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
- O-first-expt
- The first exponent of an ordinal
- Getpropc
- Access fast property lists
- Fix
- Coerce to a number
- 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
- Rfix
- Coerce to a rational 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
- *standard-ci*
- An ACL2 character-based analogue of CLTL's
*standard-input* - Unary-/
- Reciprocal function
- 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
- 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
- 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
- Denominator
- Divisor of a ratio in lowest terms
- Char>=
- Greater-than-or-equal test for characters
- Cadr
`car`of the`cdr`- 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.
- Good-atom-listp
- Recognizer for a true list of ``good'' atoms
- 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
- Min
- The smaller of two numbers
- Lognor
- Bitwise logical `nor' of two integers
- Listp
- Recognizer for (not necessarily proper) lists
- 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
- Packn
- Build a symbol from a list
- 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 - 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
- Access
- Accessor macro for defrec structures.
- 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
- 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` - Packn-pos
- Build a symbol in a specified package from a list
- 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)
- 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
- Cddr
`cdr`of the`cdr`- 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