1.4.8 Lists

(cons x y)

Creates a new pair containing x and y.

Examples:

> (cons 1 nil)

'(1)

> (cons 2 (cons 3 nil))

'(2 3)

> (cons 4 5)

'(4 . 5)

(consp x)

Returns true when x is a pair.

Examples:

> (consp nil)

'()

> (consp 5)

'()

> (consp "string")

'()

> (consp (cons 1 nil))

't

> (consp '(1 2 3))

't

(car x) → t

x : (or (consp x) (equal x nil))

Returns the first element of a cons-pair, or nil for nil.

Examples:

> (car '(1 2 4 6))

1

> (car nil)

'()

(cdr x) → t

x : (or (consp x) (equal x nil))

Returns the second element of a cons-pair, or nil for nil.

Examples:

> (cdr '(1 2 4 6))

'(2 4 6)

> (cdr nil)

'()

(append lst ...)

Concatenates all the elements in the given lists into one list. This a macro that expands into calls of the function binary-append.

Examples:

> (append nil nil)

'()

> (append nil (list 1 2))

'(1 2)

> (append (list 1 2) (list 3 4))

'(1 2 3 4)

(binary-append x y) → t

x : (true-listp x)

y : t

Concatenates two lists. Returns a new list containing all the items from x followed by all the items from y.

Examples:

> (binary-append (list 1 2 3) (list 4 5 6))

'(1 2 3 4 5 6)

> (binary-append (list 1 2 3) 4)

'(1 2 3 . 4)

> (binary-append 5 "<-error")

/Users/cce/git/release/all/trunk/planet/dracula/lang/primiti

ve-procedures/acl2-prims.ss: (region Dracula Program) broke

the contract (xargs :guard (true-listp x)) on

binary-append;

x = 5

y = "<-error"

(mv x ...)

Form for returning multiple values. This is like list, but with the restriction that if a function returns using mv, then it must always return the same number of values.

Example:

> (mv 1 2 3 4)

'(1 2 3 4)

(revappend x y) → t

x : (true-listp x)

y : t

append the reverse of x to y.

Examples:

> (revappend nil nil)

'()

> (revappend nil (list 1 2))

'(1 2)

> (revappend (list 1 2) (list 3 4))

'(2 1 3 4)

> (revappend (list 1 2) 3)

'(2 1 . 3)

(list elem ...)

Creates a new true list containing all the given elements.

Examples:

> (list)

'()

> (list 1 2 3)

'(1 2 3)

(list* elem ... tail)

Uses cons to add each elem to tail.

Examples:

> (list* 1 2 nil)

'(1 2)

> (list* 5 6 '(7 8 9))

'(5 6 7 8 9)

> (list* 1 2 3)

'(1 2 . 3)

(atom-listp x) → t

x : t

Reports whether x is a list of atoms.

Examples:

> (atom-listp (list 2 3 4))

't

> (atom-listp (list (list 23 34) 45))

'()

(character-listp x) → t

x : t

Reports whether x is a list of characterp elements.

Examples:

> (character-listp (list #\a #\b))

't

> (character-listp (list #\a "b"))

'()

(endp x) → t

x : (or (consp lst) (equal x nil))

Same as atom, but with the guard that x is either a consp or is nil.

Examples:

> (endp nil)

't

> (endp (cons 2 nil))

'()

(eqlable-listp x) → t

x : t

Reports whether x is a list of eqlablep elements.

Examples:

> (eqlable-listp nil)

't

> (eqlable-listp (cons 4 nil))

't

> (eqlable-listp t)

'()

(integer-listp x) → t

x : t

Reports whether x is a list of integerp elements.

Examples:

> (integer-listp nil)

't

> (integer-listp (list 24 -21 95))

't

> (integer-listp (list 53 44 "number"))

'()

(keyword-value-listp x) → t

x : t

Reports whether x is of even length and every other element in the list satisfies keywordp.

Examples:

> (keyword-value-listp (list :a 1 :b 2 :c 3))

't

> (keyword-value-listp (list 'a 1 'b 'c 3))

'()

(listp x) → t

x : t

Reports whether x is either a consp or nil.

Examples:

> (listp nil)

't

> (listp (cons 4 nil))

't

> (listp t)

'()

(null x) → t

x : t

Returns true if x equals nil (using eq).

Examples:

> (null nil)

't

> (null (list 1 2 3))

'()

(proper-consp x) → t

x : t

Reports whether x is a proper (nil-terminated) nonempty list

Examples:

> (proper-consp nil)

'()

> (proper-consp (list 1 2 3))

't

> (proper-consp (cons 1 2))

'()

(rational-listp x) → t

x : t

Reports whether x is a list of rationalp elements.

Examples:

> (rational-listp (list 1 2/5 3))

't

> (rational-listp (list 1 2/5 "number"))

'()

(standard-char-listp x) → t

x : t

Reports whether x is a list of standard-char-p elements.

Examples:

> (standard-char-listp (list #\a #\b #\c))

't

> (standard-char-listp (list 1 2 3))

'()

(string-listp x) → t

x : t

Reports whether x is a list of stringp elements.

Examples:

> (string-listp (list "ab" "cd" "ef"))

't

> (string-listp (list 1 2 3))

'()

(symbol-listp x) → t

x : t

Reports whether x is a list of symbolp elements.

Examples:

> (symbol-listp (list 'ab 'cd 'ef))

't

> (symbol-listp (list 1 2 3))

'()

(true-list-listp x) → t

x : t

Reports whether x is a list of true-listp elements.

Examples:

> (true-list-listp (list 1 2 3 4 5))

'()

> (true-list-listp '((1) (2) (3) (4) (5)))

't

(true-listp x) → t

x : t

Reports whether x is a proper nil-terminated list.

Examples:

> (true-listp (list 1 2 3 4 5))

't

> (true-listp "list")

'()

(butlast l n) → t

l : (true-listp l)

n : (and (integerp n) (<= 0 n))

(butlast l n) is the list obtained by removing the last n elements from the true list l.

Examples:

> (butlast (list 1 2 3) 1)

'(1 2)

> (butlast (list 1 2 3) 2)

'(1)

> (butlast (list 1 2 3) 3)

'()

(fix-true-list x) → t

x : t

Coerces x to a true list by replacing the final cdr with nil.

Examples:

> (fix-true-list (list 1 2 3))

'(1 2 3)

> (fix-true-list (cons 1 (cons 2 3)))

'(1 2)

> (fix-true-list "abc")

'()

> (fix-true-list 5)

'()

(len lst) → t

lst : t

Finds the length of the given list. Returns 0 if lst is not a list.

Examples:
> (len nil)
0
> (len (list 1 2 3 4 5))
5
> (len "string")
0
> (len t)
0

(make-list n) → true-listp

n : (and (integerp n) (<= 0 n))

Makes a list of the given length, filling it in with nil.

Examples:

> (make-list 0)

'()

> (make-list 3)

'(() () ())

(nth n lst) → t

n : (and (integerp n) (>= n 0))

lst : (true-listp lst)

Gets the nth element of lst

Examples:

> (nth 2 (list 1 2 3))

3

> (nth 4 (list 1 2 1))

'()

(nthcdr n lst) → t

n : (and (integerp n) (>= n 0))

lst : (true-listp lst)

Gets the nth cdr of the given list

Examples:

> (nthcdr 2 (list 1 2 3))

'(3)

> (nthcdr 3 (list 1 2 1))

'()

(reverse x) → t

x : (or (true-listp x) (stringp x))

Reverse the given list or string

Examples:

> (reverse (list 1 2 3 4))

'(4 3 2 1)

> (reverse "abcd")

"dcba"

(take n l) → t

n : (and (integerp n) (not (< n 0)))

l : (true-listp l)

Examples:

> (take 3 (list 1 2 3 4 5))

'(1 2 3)

> (take 0 (list 1 2 3 4 5))

'()

(update-nth n v lst) → t

n : (and (integerp n) (<= 0 n))

v : t

lst : (true-listp l)

Replaces the nth (0-based) position in lst with the value v. If n is greater than the length of lst, then update-nth will add padding to the end of the list consisting of nil values.

Examples:

> (update-nth 0 'z '(a b c d e))

'(z b c d e)

> (update-nth 8 'z '(a b c d e))

'(a b c d e () () () z)

(first lst)

first member of the list

Example:

> (first (list 1 2 3 4 5 6 7 8))

1

(second lst)

Example:

> (second (list 1 2 3 4 5))

2

(third lst)

Example:

> (third (list 1 2 3 4 5 6 7 8 9 10))

3

(fourth lst)

fourth member of the list

Example:

> (fourth (list 1 2 3 4 5 6 7 8))

4

(fifth lst)

fifth member of the list

Example:

> (fifth (list 1 2 3 4 5 6 7 8))

5

(sixth lst)

Sixth member of the list

Example:

> (sixth (list 1 2 3 4 5 6 7 8 9 10))

6

(seventh lst)

Example:

> (seventh (list 1 2 3 4 5 6 7 8 9 10))

7

(eighth lst)

eighth member of the list

Example:

> (eighth (list 1 2 3 4 5 6 7 8))

8

(ninth x)

Example:

> (ninth (list 1 2 3 4 5 6 7 8 9 10))

9

(tenth lst)

Example:

> (tenth (list 1 2 3 4 5 6 7 8 9 10))

10

(last lst)

last member of the list

Example:

> (last (list 1 2 3 4 5))

'(5)

(rest lst)

The same as cdr

Example:

> (rest (list 'w 'x 'y 'z))

'(x y z)

1	ACL2
2	Teachpacks
3	Modular ACL2
	Index

1.1	Data Types
1.2	Expressions
1.3	Events and Definitions
1.4	Functions and Macros
1.5	Theorem Prover Controls
1.6	ACL2 Books
1.7	Unsupported

1.4.1	Booleans
1.4.2	Symbols
1.4.3	Strings
1.4.4	Characters
1.4.5	Rational and Complex Arithmetic
1.4.6	Bitwise Operations
1.4.7	Ordinal Arithmetic
1.4.8	Lists
1.4.9	Association Lists
1.4.10	Sets
1.4.11	Trees
1.4.12	Sequences
1.4.13	IO