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