		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
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, 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
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 suitable cons 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 ith 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
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
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) causes name to be a fast alist for the execution of form.
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, returning alist 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 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
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 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
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 cdrs 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