## SYMBOLP

recognizer for symbols
```Major Section:  PROGRAMMING
```

`(symbolp x)` is true if and only if `x` is a symbol.

## TAKE

initial segment of a list
```Major Section:  PROGRAMMING
```

For any natural number `n` not exceeding the length of `l`, `(take n l)` collects the first `n` elements of the list `l`.

The following is a theorem (though it takes some effort, including lemmas, to get ACL2 to prove it):

```(equal (length (take n l)) (nfix n))
```
If `n` is is an integer greater than the length of `l`, then `take` pads the list with the appropriate number of `nil` elements. Thus, the following is also a theorem.
```(implies (and (integerp n)
(true-listp l)
(<= (length l) n))
(equal (take n l)
(append l (make-list (- n (length l))))))
```
For related functions, see nthcdr and see butlast.

The guard for `(take n l)` is that `n` is a nonnegative integer and `l` is a true list.

## TENTH

tenth member of the list
```Major Section:  PROGRAMMING
```

See any Common Lisp documentation for details.

## THE

run-time type check
```Major Section:  PROGRAMMING
```

`(The typ val)` checks that `val` satisfies the type specification `typ` (see type-spec). An error is caused if the check fails, and otherwise, `val` is the value of this expression. Here are some examples.

```(the integer 3)       ; returns 3
(the (integer 0 6) 3) ; returns 3
(the (integer 0 6) 7) ; causes an error
```
See type-spec for a discussion of the legal type specifications.

`The` is defined in Common Lisp. See any Common Lisp documentation for more information.

## THIRD

third member of the list
```Major Section:  PROGRAMMING
```

See any Common Lisp documentation for details.

## TRUE-LIST-LISTP

recognizer for true (proper) lists of true lists
```Major Section:  PROGRAMMING
```

`True-list-listp` is the function that checks whether its argument is a list that ends in, or equals, `nil`, and furthermore, all of its elements have that property. Also see true-listp.

## TRUE-LISTP

recognizer for proper (null-terminated) lists
```Major Section:  PROGRAMMING
```

`True-listp` is the function that checks whether its argument is a list that ends in, or equals, `nil`.

## TRUNCATE

division returning an integer by truncating toward 0
```Major Section:  PROGRAMMING
```

```Example Forms:
ACL2 !>(truncate 14 3)
4
ACL2 !>(truncate -14 3)
-4
ACL2 !>(truncate 14 -3)
-4
ACL2 !>(truncate -14 -3)
4
ACL2 !>(truncate -15 -3)
5
```
`(Truncate i j)` is the result of taking the quotient of `i` and `j` and dropping the fraction. For example, the quotient of `-14` by `3` is `-4 2/3`, so dropping the fraction `2/3`, we obtain a result for `(truncate -14 3)` of `-4`.

The guard for `(truncate i j)` requires that `i` and `j` are rational (real, in ACL2(r)) numbers and `j` is non-zero.

`Truncate` is a Common Lisp function. See any Common Lisp documentation for more information.

## TYPE-SPEC

type specifiers in declarations
```Major Section:  PROGRAMMING
```

```Examples:
The symbol INTEGER in (declare (type INTEGER i j k)) is a type-spec.  Other
type-specs supported by ACL2 include RATIONAL, COMPLEX, (INTEGER 0 127),
(RATIONAL 1 *), CHARACTER, and ATOM.
```

The type-specs and their meanings (when applied to the variable `x` as in `(declare (type type-spec x))` are given below.

```type-spec                 meaning
ATOM                 (ATOM X)
BIT                  (OR (EQUAL X 1) (EQUAL X 0))
CHARACTER            (CHARACTERP X)
COMPLEX,             (AND (COMPLEX-RATIONALP X)
(COMPLEX RATIONAL)        (RATIONALP (REALPART X))
(RATIONALP (IMAGPART X)))
(COMPLEX type)       (AND (COMPLEX-RATIONALP X)
(p (REALPART X))
(p (IMAGPART X)))
where (p x) is the meaning for type-spec type
CONS                 (CONSP X)
INTEGER              (INTEGERP X)
(INTEGER i j)        (AND (INTEGERP X)   ; See notes below
(<= i X)
(<= X j))
(MEMBER x1 ... xn)   (MEMBER X '(x1 ... xn))
(MOD i)              same as (INTEGER 0 i-1)
NIL                  NIL
NULL                 (EQ X NIL)
RATIO                (AND (RATIONALP X) (NOT (INTEGERP X)))
RATIONAL             (RATIONALP X)
(RATIONAL i j)       (AND (RATIONALP X)  ; See notes below
(<= i X)
(<= X j))
REAL                 (RATIONALP X)       ; (REALP X) in ACL2(r)
(REAL i j)           (AND (RATIONALP X)  ; See notes below
(<= i X)
(<= X j))
(SATISFIES pred)     (pred X)
SIGNED-BYTE          (INTEGERP X)
(SIGNED-BYTE i)      same as (INTEGER -2**i-1 (2**i-1)-1)
STANDARD-CHAR        (STANDARD-CHARP X)
STRING               (STRINGP X)
(STRING max)         (AND (STRINGP X) (EQUAL (LENGTH X) max))
SYMBOL               (SYMBOLP X)
T                    T
UNSIGNED-BYTE        same as (INTEGER 0 *)
(UNSIGNED-BYTE i)    same as (INTEGER 0 (2**i)-1)
```
Notes:

In general, `(integerp i j)` means

```     (AND (INTEGERP X)
(<= i X)
(<= X j)).
```
But if `i` is the symbol `*`, the first inequality is omitted. If `j` is the symbol `*`, the second inequality is omitted. If instead of being an integer, the second element of the type specification is a list containing an integer, `(i)`, then the first inequality is made strict. An analogous remark holds for the `(j)` case. The `RATIONAL` and `REAL` type specifiers are similarly generalized.

## UNARY--

arithmetic negation function
```Major Section:  PROGRAMMING
```

Completion Axiom:

```(equal (unary-- x)
(if (acl2-numberp x)
(unary-- x)
0))
```

Guard for `(unary-- x)`:

```(acl2-numberp x)
```
Notice that like all arithmetic functions, `unary--` treats non-numeric inputs as `0`.

Calls of the macro `-` on one argument expand to calls of `unary--`; see -.

## UNARY-/

reciprocal function
```Major Section:  PROGRAMMING
```

Completion Axiom:

```(equal (unary-/ x)
(if (and (acl2-numberp x)
(not (equal x 0)))
(unary-/ x)
0))
```

Guard for `(unary-/ x)`:

```(and (acl2-numberp x)
(not (equal x 0)))
```
Notice that like all arithmetic functions, `unary-/` treats non-numeric inputs as `0`.

Calls of the macro `/` on one argument expand to calls of `unary-/`; see /.

## UNION-EQ

union of two lists of symbols
```Major Section:  PROGRAMMING
```

`(Union-eq x y)` equals a list whose members (see member-eq) contains the members of `x` and the members of `y`. More precisely, the resulting list is the same as one would get by first deleting the members of `y` from `x`, and then concatenating the result to the front of `y`.

The guard for `union-eq` requires both arguments to be true lists, but in fact further requires the first list to contain only symbols, as the function `member-eq` is used to test membership (with `eq`). See union-equal.

## UNION-EQUAL

union of two lists
```Major Section:  PROGRAMMING
```

`(Union-equal x y)` equals a list whose members (see member-equal) contains the members of `x` and the members of `y`. More precisely, the resulting list is the same as one would get by first deleting the members of `y` from `x`, and then concatenating the result to the front of `y`.

The guard for `union-equal` requires both arguments to be true lists. Essentially, `union-equal` has the same functionality as the Common Lisp function `union`, except that it uses the `equal` function to test membership rather than `eql`. However, we do not include the function `union` in ACL2, because the Common Lisp language does not specify the order of the elements in the list that it returns.

## UPDATE-NTH

modify a list by putting the given value at the given position
```Major Section:  PROGRAMMING
```

`(Update-nth key val l)` returns a list that is the same as the list `l`, except that the value at the `0`-based position `key` (a natural number) is `val`.

If `key` is an integer at least as large as the length of `l`, then `l` will be padded with the appropriate number of `nil` elements, as illustrated by the following example.

```ACL2 !>(update-nth 8 'z '(a b c d e))
(A B C D E NIL NIL NIL Z)
```
We have the following theorem.
```(implies (and (true-listp l)
(integerp key)
(<= 0 key))
(equal (length (update-nth key val l))
(if (< key (length l))
(length l)
(+ 1 key))))
```

The guard of `update-nth` requires that its first (position) argument is a natural number and its last (list) argument is a true list.

## UPPER-CASE-P

recognizer for upper case characters
```Major Section:  PROGRAMMING
```

`(Upper-case-p x)` is true if and only if `x` is an upper case character, i.e., a member of the list `#A`, `#B`, ..., `#Z`.

The guard for `upper-case-p` requires its argument to be a character.

`Upper-case-p` is a Common Lisp function. See any Common Lisp documentation for more information.

## ZERO-TEST-IDIOMS

how to test for 0
```Major Section:  PROGRAMMING
```

Below are six commonly used idioms for testing whether `x` is `0`. `Zip` and `zp` are the preferred termination tests for recursions down the integers and naturals, respectively.

```idiom       logical              guard              primary
meaning                              compiled code*

(equal x 0)(equal x 0)          t                (equal x 0)

(eql x 0)  (equal x 0)          t                (eql x 0)

(zerop x)  (equal x 0)          x is a number    (= x 0)

(= x 0)    (equal x 0)          x is a number    (= x 0)

(zip x)    (equal (ifix x) 0)   x is an integer  (= x 0)

(zp x)     (equal (nfix x) 0)   x is a natural   (= x 0)
```
*See guards-and-evaluation, especially the subsection titled ``Guards and evaluation V: efficiency issues''. Primary code is relevant only if guards are verified. The ``compiled code'' shown is only suggestive.

The first four idioms all have the same logical meaning and differ only with respect to their executability and efficiency. In the absence of compiler optimizing, `(= x 0)` is probably the most efficient, `(equal x 0)` is probably the least efficient, and `(eql x 0)` is in between. However, an optimizing compiler could always choose to compile `(equal x 0)` as `(eql x 0)` and, in situations where `x` is known at compile-time to be numeric, `(eql x 0)` as `(= x 0)`. So efficiency considerations must, of course, be made in the context of the host compiler.

Note also that `(zerop x)` and `(= x 0)` are indistinguishable. They have the same meaning and the same guard, and can reasonably be expected to generate equally efficient code.

Note that `(zip x)` and `(zp x)` do not have the same logical meanings as the others or each other. They are not simple tests for equality to `0`. They each coerce `x` into a restricted domain, `zip` to the integers and `zp` to the natural numbers, choosing `0` for `x` when `x` is outside the domain. Thus, `1/2`, `#c(1 3)`, and `'abc`, for example, are all ``recognized'' as zero by both `zip` and `zp`. But `zip` reports that `-1` is different from `0` while `zp` reports that `-1` ``is'' `0`. More precisely, `(zip -1)` is `nil` while `(zp -1)` is `t`.

Note that the last four idioms all have guards that restrict their Common Lisp executability. If these last four are used in situations in which guards are to be verified, then proof obligations are incurred as the price of using them. If guard verification is not involved in your project, then the first four can be thought of as synonymous.

`Zip` and `zp` are not provided by Common Lisp but are ACL2-specific functions. Why does ACL2 provide these functions? The answer has to do with the admission of recursively defined functions and efficiency. `Zp` is provided as the zero-test in situations where the controlling formal parameter is understood to be a natural number. `Zip` is analogously provided for the integer case. We illustrate below.

Here is an admissible definition of factorial

```(defun fact (n) (if (zp n) 1 (* n (fact (1- n)))))
```
Observe the classic recursion scheme: a test against `0` and recursion by `1-`. Note however that the test against `0` is expressed with the `zp` idiom. Note also the absence of a guard making explicit our intention that `n` is a natural number.

This definition of factorial is readily admitted because when `(zp n)`

is false (i.e., `nil`) then `n` is a natural number other than `0` and so `(1- n)` is less than `n`. The base case, where `(zp n)` is true, handles all the ``unexpected'' inputs, such as arise with `(fact -1)` and `(fact 'abc)`. When calls of `fact` are evaluated, `(zp n)` checks `(integerp n)` and `(> n 0)`. Guard verification is unsuccessful for this definition of `fact` because `zp` requires its argument to be a natural number and there is no guard on `fact`, above. Thus the primary raw lisp for `fact` is inaccessible and only the `:``logic` definition (which does runtime ``type'' checking) is used in computation. In summary, this definition of factorial is easily admitted and easily manipulated by the prover but is not executed as efficiently as it could be.

Runtime efficiency can be improved by adding a guard to the definition.

```(defun fact (n)
(declare (xargs :guard (and (integerp n) (>= n 0))))
(if (zp n) 1 (* n (fact (1- n)))))
```
This guarded definition has the same termination conditions as before -- termination is not sensitive to the guard. But the guards can be verified. This makes the primary raw lisp definition accessible during execution. In that definition, the `(zp n)` above is compiled as `(= n 0)`, because `n` will always be a natural number when the primary code is executed. Thus, by adding a guard and verifying it, the elegant and easily used definition of factorial is also efficiently executed on natural numbers.

Now let us consider an alternative definition of factorial in which `(= n 0)` is used in place of `(zp n)`.

```(defun fact (n) (if (= n 0) 1 (* n (fact (1- n)))))
```
This definition does not terminate. For example `(fact -1)` gives rise to a call of `(fact -2)`, etc. Hence, this alternative is inadmissible. A plausible response is the addition of a guard restricting `n` to the naturals:
```(defun fact (n)
(declare (xargs :guard (and (integerp n) (>= n 0))))
(if (= n 0) 1 (* n (fact (1- n)))))
```
But because the termination argument is not sensitive to the guard, it is still impossible to admit this definition. To influence the termination argument one must change the conditions tested. Adding a runtime test that `n` is a natural number would suffice and allow both admission and guard verification. But such a test would slow down the execution of the compiled function.

The use of `(zp n)` as the test avoids this dilemma. `Zp` provides the logical equivalent of a runtime test that `n` is a natural number but the execution efficiency of a direct `=` comparison with `0`, at the expense of a guard conjecture to prove. In addition, if guard verification and most-efficient execution are not needed, then the use of `(zp n)` allows the admission of the function without a guard or other extraneous verbiage.

While general rules are made to be broken, it is probably a good idea to get into the habit of using `(zp n)` as your terminating ```0` test'' idiom when recursing down the natural numbers. It provides the logical power of testing that `n` is a non-`0` natural number and allows efficient execution.

We now turn to the analogous function, `zip`. `Zip` is the preferred `0`-test idiom when recursing through the integers toward `0`. `Zip` considers any non-integer to be `0` and otherwise just recognizes `0`. A typical use of `zip` is in the definition of `integer-length`, shown below. (ACL2 can actually accept this definition, but only after appropriate lemmas have been proved.)

```(defun integer-length (i)
(declare (xargs :guard (integerp i)))
(if (zip i)
0
(if (= i -1)
0
(+ 1 (integer-length (floor i 2))))))
```
Observe that the function recurses by `(floor i 2)`. Hence, calling the function on `25` causes calls on `12`, `6`, `3`, `1`, and `0`, while calling it on `-25` generates calls on `-13`, `-7`, `-4`, `-2`, and `-1`. By making `(zip i)` the first test, we terminate the recursion immediately on non-integers. The guard, if present, can be verified and allows the primary raw lisp definition to check `(= i 0)` as the first terminating condition (because the primary code is executed only on integers).

## ZEROP

test an acl2-number against 0
```Major Section:  PROGRAMMING
```

`(zerop x)` is `t` if `x` is `0` and is `nil` otherwise. Thus, it is logically equivalent to `(equal x 0)`.

`(Zerop x)` has a guard requiring `x` to be numeric and can be expected to execute more efficiently than `(equal x 0)` in properly guarded compiled code.

In recursions down the natural numbers, `(zp x)` is preferred over `(zerop x)` because the former coerces `x` to a natural and allows the termination proof. In recursions through the integers, `(zip x)` is preferred. See zero-test-idioms.

`Zerop` is a Common Lisp function. See any Common Lisp documentation for more information.

## ZIP

testing an ``integer'' against 0
```Major Section:  PROGRAMMING
```

`(Zip i)` is logically equivalent to `(equal (ifix i) 0)` and is the preferred termination test for recursion through the integers. `(Zip i)` returns `t` if `i` is `0` or not an integer; it returns `nil` otherwise. Thus,

```    i       (zp i)
3         nil
0         t
-2        nil
5/2       t
#c(1 3)   t
'abc      t
```

`(Zip i)` has a guard requiring `i` to be an integer.

For a discussion of the various idioms for testing against `0`, see zero-test-idioms.

`Zip` is typically used as the termination test in recursions through the integers. It has the advantage of ``coercing'' its argument to an integer and hence allows the definition to be admitted without an explicit type check in the body. Guard verification allows `zip` to be compiled as a direct `=`-comparision with `0`.

## ZP

testing a ``natural'' against 0
```Major Section:  PROGRAMMING
```

`(Zp n)` is logically equivalent to `(equal (nfix n) 0)` and is the preferred termination test for recursion down the natural numbers. `(Zp n)` returns `t` if `n` is `0` or not a natural number; it returns `nil` otherwise. Thus, in the ACL2 logic (ignoring the issue of guards):

```    n       (zp n)
3         nil
0         t
-1        t
5/2       t
#c(1 3)   t
'abc      t
```

`(Zp n)` has a guard requiring `n` to be a natural number.

For a discussion of the various idioms for testing against `0`, see zero-test-idioms.

`Zp` is typically used as the termination test in recursions down the natural numbers. It has the advantage of ``coercing'' its argument to a natural and hence allows the definition to be admitted without an explicit type check in the body. Guard verification allows `zp` to be compiled as a direct `=`-comparision with `0`.