▼ACL2s Beginner Mode
On this page:
tl
listof
tlp
cons
endp
consp
first
rest
list
len
app
rev
in
  top  ← prev  up  next → 

5 Lists and Pairs

type

tl

type

(listof X)

procedure

(tlp v) → boolean

  v : all
Produces t if v is a true list, nil otherwise. A true list is either nil or a cons pair with a true list in the rest position.

> (tlp nil)

t

> (tlp (cons 1 (cons 2 (cons 3 nil))))

t

> (tlp "lime")

nil

; if it doesn't end with nil, it's not a true list:
> (tlp (cons 1 (cons 2 3)))

nil

value

nil : (listof X)

The empty list. Every list has nil at the end.

> nil

nil

> (list)

nil

> (cons 1 nil)

(list 1)

> (list 1)

(list 1)

> (rest (cons 1 nil))

nil

Warning: nil happens to be an empty list, a boolean, and a symbol all at once, so be careful when mixing these types together.

> (tlp nil)

t

> (booleanp nil)

t

> (symbolp nil)

t

procedure

(cons x y) → (listof X)

  x : X
  y : (listof X)
(cons x y) → (cons X Y)
  x : X
  y : Y
Constructs a pair. The x argument is the first, and the y argument is the rest.

If you want to make a list, then y should be a list.

> (cons 5 nil)

(list 5)

> (cons 2 (cons 4 (cons 8 nil)))

(list 2 4 8)

> (cons 3 (list 5 7 11 13))

(list 3 5 7 11 13)

A cons is not always a list. It’s only a list when the rest is also a list.

> (tlp (cons 1 (cons 2 (cons 3 (cons 4 nil)))))

t

; please never do this:
> (tlp (cons 1 (cons 2 (cons 3 4))))

nil

procedure

(endp l) → boolean

  l : (listof X)
Produces t if the list l is empty, nil otherwise.

> (endp nil)

t

> (endp (cons 1 (cons 2 (cons 3 nil))))

nil

procedure

(consp v) → boolean

  v : all
Produces t if the v is a cons pair, nil otherwise.

> (consp nil)

nil

> (consp (cons 1 (cons 2 (cons 3 nil))))

t

> (consp "banana")

nil

procedure

(first lst) → X

  lst : (listof X)
(first pair) → X
  pair : (cons X Y)
Gets the first element of a list or pair.

> (first (cons 5 nil))

5

> (first (cons 1 (cons 2 (cons 3 nil))))

1

> (first (list "apple" "banana" "cherry"))

"apple"

procedure

(rest lst) → (listof X)

  lst : (listof X)
(rest pair) → Y
  pair : (cons X Y)
Gets the rest of a list or pair.

> (rest (cons 5 nil))

nil

> (rest (cons 1 (cons 2 (cons 3 nil))))

(list 2 3)

> (rest (list "apple" "banana" "cherry"))

(list "banana" "cherry")

procedure

(list x ...) → (listof X)

  x : X
Produces a list with all the xs.

> (list)

nil

> (list 1 2 3)

(list 1 2 3)

> (list "red" "orange" "yellow" "green" "blue" "purple")

(list "red" "orange" "yellow" "green" "blue" "purple")

procedure

(len l) → nat

  l : (listof X)
Produces the length of the list.

> (len nil)

0

> (len (list 1 2 3))

3

> (len (list 'a 'b 'c 'd 'e 'f 'g))

7

procedure

(app a b) → (listof X)

  a : (listof X)
  b : (listof X)
Appends the lists a and b together into a new list with the elements of a first and the elements of b after that.

> (app nil (list 3 5 8))

(list 3 5 8)

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

(list 1 2 3 4 5)

> (app (list 'a) (list 'b 'c))

(list 'a 'b 'c)

> (app (app (list 'a) (list 'b 'c)) (list 'd 'e 'f 'g))

(list 'a 'b 'c 'd 'e 'f 'g)

procedure

(rev l) → (listof X)

  l : (listof X)
Reverses the list l.

> (rev nil)

nil

> (rev (list 1 2 3))

(list 3 2 1)

> (rev (list 'a 'b 'c 'd 'e 'f 'g))

(list 'g 'f 'e 'd 'c 'b 'a)

procedure

(in a l) → boolean

  a : all
  l : tl
Produces t if the list l contains the value a somewhere in it (according to equal).

> (in 2 (list 1 2 3))

t

> (in 2 (list 1 3 5))

nil

> (in 'g (list 'c 'a 'b 'b 'a 'g 'e))

t

> (in 'g (list 'c 'a 'b 'b 'a 'j 'e))

nil

  top  ← prev  up  next →