		Search-engine friendly clone of the ACL2 documentation.

Programming

ACL2-built-ins

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

Subtopics

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
Defwarrant: Issue a warrant for a function so apply$ can use it in proofs
Ec-call: Execute a call in the ACL2 logic instead of raw Lisp
Sys-call: Make a system call to the host operating system
Mv-nth: The mv-nth element (zero-based) of a list
Value-triple: Compute a value, optionally checking that it is not nil
Msg: Construct a ``message'' suitable for the ~@ directive of fmt
Comp: Compile some ACL2 functions
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
Er: Print an error message and ``cause an error''
*ACL2-exports*: Symbols that are often imported into new packages to provide easy access to ACL2 functionality.
Defbadge: Issue a badge for a function so apply$ can evaluate with it
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
Posp: A recognizer for the positive integers
Nth: The nth element (zero-based) of a list
And: Conjunction
Flet: Local binding of function symbols
Unsigned-byte-p: Recognizer for natural numbers that fit in a specified bit width
Len: Length of a list
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
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
Bitp: A recognizer for the set of bits, {0,1}
Equal: True equality
Cdr: Returns the second element of a cons pair, else nil
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
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
<: Less-than
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.
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
Let*: Binding of lexically scoped (local) variables
Length: Length of a string or proper list
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
-: Macro for subtraction and negation
Pand: Parallel, Boolean version of and
Cons-with-hint: Alternative to cons that tries to avoid consing when a suitable cons structure is provided as a hint.
Case-match: Pattern matching or destructuring
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.
Symbol-name: The name of a symbol (a string)
Remove-duplicates: Remove duplicates from a string or a list
With-serialize-character: Control output mode for print-object$
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
ACL2-count: A commonly used measure for justifying recursion
Position: Position of an item in a string or a list
Termp: recognizer for the quotation of a term
Logbitp: The ith 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
Assoc: Look up key in association list
Get-internal-time: Runtime vs. realtime in ACL2 timings
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
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
Expt: Exponential function
Non-exec: Mark code as non-executable
Keywordp: Recognizer for keywords
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
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
Ash: Arithmetic shift operation
With-fast-alist: (with-fast-alist name form) causes name to be a fast alist for the execution of form.
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
Rationalp: Recognizer for rational numbers (ratios and integers)
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
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
Mv-list: Converting multiple-value result to a single-value 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
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
Symbol-alistp: Recognizer for association lists with symbols as keys
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.
Canonical-pathname: The true absolute filename, with soft links resolved
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
<=: Less-than-or-equal test
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
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
Princ$: Print an atom
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
Cond: Conditional based on if-then-else
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
Truncate: Division returning an integer by truncating toward 0
Reverse: Reverse a list or string
Endp: Recognizer for empty lists
Code-char: The character corresponding to a given numeric code
Setenv$: Set an environment variable
Print-object$: Print an 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 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
Integer-listp: Recognizer for a true list of integers
Boole$: Perform a bit-wise logical operation on 2 two's complement integers
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, returning alist 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
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
Pairlis$: Zipper together two lists
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 that name is a fast alist at the start of the execution of form. At the end of execution, it ensures that name is a fast alist if and only if it was originally. That is, if name 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 of form, that table is restored. Note that any extended table created from the original fast alist during form must be manually freed.
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
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
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
Pos-listp: Recognizer for a true list of positive integers
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
String-equal: String equality without regard to case
List*: Build a list
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
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
Rfix: Coerce to a rational number
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
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
Er-soft: Print an error message and ``cause a soft error''
Eqlable-alistp: Recognizer for a true list of pairs whose cars 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
Cadr: car of the cdr
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
Listp: Recognizer for (not necessarily proper) lists
Denominator: Divisor of a ratio in lowest terms
Char>=: Greater-than-or-equal test for characters
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
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 cdrs 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
Cddr: cdr of the cdr
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