## LOGAND

bitwise logical `and' of two integers
```Major Section:  PROGRAMMING
```

When integers are viewed in their two's complement representation, `logand` returns their bitwise logical `and'.

The guard for `logand` requires its arguments to be integers. `Logand` is defined in Common Lisp. See any Common Lisp documentation for more information.

## LOGANDC1

bitwise logical `and' of two ints, complementing the first
```Major Section:  PROGRAMMING
```

When integers are viewed in their two's complement representation, `logandc1` returns the bitwise logical `and' of the second with the bitwise logical `not' of the first.

The guard for `logandc1` requires its arguments to be integers. `Logandc1` is defined in Common Lisp. See any Common Lisp documentation for more information.

## LOGANDC2

bitwise logical `and' of two ints, complementing the second
```Major Section:  PROGRAMMING
```

When integers are viewed in their two's complement representation, `logandc2` returns the bitwise logical `and' of the first with the bitwise logical `not' of the second.

The guard for `logandc2` requires its arguments to be integers. `Logandc2` is defined in Common Lisp. See any Common Lisp documentation for more information.

## LOGBITP

the `i`th bit of an integer
```Major Section:  PROGRAMMING
```

For a nonnegative integer `i` and an integer `j`, `(logbitp i j)` is the value of the `i`th bit in the two's complement representation of `j`.

`(Logbitp i j)` has a guard that `i` is a nonnegative integer and `j` is an integer.

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

## LOGCOUNT

number of ``on'' bits in a two's complement number
```Major Section:  PROGRAMMING
```

`(Logcount x)` is the number of ``on'' bits in the two's complement representation of `x`.

`(Logcount x)` has a guard of `(integerp x)`.

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

## LOGEQV

bitwise logical equivalence of two integers
```Major Section:  PROGRAMMING
```

When integers are viewed in their two's complement representation, `logeqv` returns the bitwise logical equivalence of the first with the second.

The guard for `logeqv` requires its arguments to be integers. `Logeqv` is defined in Common Lisp. See any Common Lisp documentation for more information.

## LOGIOR

bitwise logical inclusive or of two integers
```Major Section:  PROGRAMMING
```

When integers are viewed in their two's complement representation, `logior` returns their bitwise logical inclusive or.

The guard for `logior` requires its arguments to be integers. `Logior` is defined in Common Lisp. See any Common Lisp documentation for more information.

## LOGNAND

bitwise logical `nand' of two integers
```Major Section:  PROGRAMMING
```

When integers are viewed in their two's complement representation, `lognand` returns their bitwise logical `nand'.

The guard for `lognand` requires its arguments to be integers. `Lognand` is defined in Common Lisp. See any Common Lisp documentation for more information.

## LOGNOR

bitwise logical `nor' of two integers
```Major Section:  PROGRAMMING
```

When integers are viewed in their two's complement representation, `lognor` returns the bitwise logical `nor' of the first with the second.

The guard for `lognor` requires its arguments to be integers. `Lognor` is defined in Common Lisp. See any Common Lisp documentation for more information.

## LOGNOT

bitwise not of a two's complement number
```Major Section:  PROGRAMMING
```

`(lognot i)` is the two's complement bitwise ``not'` of the integer `i`.

`Lognot` is actually defined by coercing its argument to an integer (see ifix), negating the result, and then subtracting `1`.

The guard for `lognot` requires its argument to be an integer.

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

## LOGORC1

bitwise logical inclusive or of two ints, complementing the first
```Major Section:  PROGRAMMING
```

When integers are viewed in their two's complement representation, `logorc1` returns the bitwise logical inclusive or of the second with the bitwise logical `not' of the first.

The guard for `logorc1` requires its arguments to be integers. `Logorc1` is defined in Common Lisp. See any Common Lisp documentation for more information.

## LOGORC2

bitwise logical inclusive or of two ints, complementing the second
```Major Section:  PROGRAMMING
```

When integers are viewed in their two's complement representation, `logorc2` returns the bitwise logical inclusive or of the first with the bitwise logical `not' of the second.

The guard for `logorc2` requires its arguments to be integers. `Logorc2` is defined in Common Lisp. See any Common Lisp documentation for more information.

## LOGTEST

test if two integers share a `1' bit
```Major Section:  PROGRAMMING
```

When integers `x` and `y` are viewed in their two's complement representation, `(logtest x y)` is true if and only if there is some position for which both `x` and `y` have a `1' bit in that position.

The guard for `logtest` requires its arguments to be integers. `Logtest` is defined in Common Lisp. See any Common Lisp documentation for more information.

## LOGXOR

bitwise logical exclusive or of two integers
```Major Section:  PROGRAMMING
```

When integers are viewed in their two's complement representation, `logxor` returns the bitwise logical exclusive or of the first with the second.

The guard for `logxor` requires its arguments to be integers. `Logxor` is defined in Common Lisp. See any Common Lisp documentation for more information.

## LOWER-CASE-P

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

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

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

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

## MAKE-CHARACTER-LIST

coerce to a list of characters
```Major Section:  PROGRAMMING
```

Non-characters in the given list are coerced to the character with code 0.

## MAKE-LIST

make a list of a given size
```Major Section:  PROGRAMMING
```

For a nonnegative integer `size`, `(Make-list size)` is a list of elements of length `size`, each of which is initialized to the `:initial-element` (which defaults to `nil`).

`Make-list` is a macro in ACL2, defined in terms of a tail recursive function `make-list-ac` whose guard requires `size` to be a nonnegative integer. `Make-list` is a Common Lisp function. See any Common Lisp documentation for more information.

## MAX

the larger of two numbers
```Major Section:  PROGRAMMING
```

`(Max x y)` is the larger of the numbers `x` and `y`.

The guard for `max` requires its arguments to be rational (real, in ACL2(r)) numbers.

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

## MEMBER

membership predicate, using `eql` as test
```Major Section:  PROGRAMMING
```

`(Member x l)` equals the longest tail of `l` that begins with `x`, or else `nil` if no such tail exists.

`(Member x l)` is provably the same in the ACL2 logic as `(member-equal x l)`. It has a stronger guard than `member-equal` because uses `eql` to test for whether `x` is equal to a given member of `l`. Its guard requires that `l` is a true list, and moreover, either `(eqlablep x)` or all members of `l` are `eqlablep`. See member-equal and see member-eq.

`Member` is a Common Lisp function. See any Common Lisp documentation for more information. Since ACL2 functions cannot take keyword arguments (though macros can), the ACL2 functions `member-equal` and `member-eq` are defined to correspond to calls of the Common Lisp function `member` whose keyword argument `:test` is `equal` or `eq`, respectively.

## MEMBER-EQ

membership predicate, using `eq` as test
```Major Section:  PROGRAMMING
```

`(Member-eq x lst)` equals the longest tail of `lst` that begins with `x`, or else `nil` if no such tail exists.

`(Member-eq x lst)` is provably the same in the ACL2 logic as `(member x lst)` and `(member-equal x lst)`, but it has a stronger guard because it uses `eq` for a more efficient test for whether `x` is equal to a given member of `lst`. Its guard requires that `lst` is a true list, and moreover, either `x` is a symbol or `lst` is a list of symbols. See member-equal and see member.

## MEMBER-EQUAL

membership predicate
```Major Section:  PROGRAMMING
```

`(Member-equal x lst)` equals the longest tail of `lst` that begins with `x`, or else `nil` if no such tail exists.

`(Member-equal x lst)` has a guard of `(true-listp lst)`. `Member-equal` has the same functionality as the Common Lisp function `member`, except that it uses the `equal` function to test whether `x` is the same as each successive element of `lst`. See member and see member-eq.

## MIN

the smaller of two numbers
```Major Section:  PROGRAMMING
```

`(Min x y)` is the smaller of the numbers `x` and `y`.

The guard for `min` requires its arguments to be rational (real, in ACL2(r)) numbers.

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

## MINUSP

test whether a number is negative
```Major Section:  PROGRAMMING
```

`(Minusp x)` is true if and only if `x < 0`.

The guard of `minusp` requires its argument to be a rational (real, in ACL2(r)) number.

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

## MOD

remainder using `floor`
```Major Section:  PROGRAMMING
```

```ACL2 !>(mod 14 3)
2
ACL2 !>(mod -14 3)
1
ACL2 !>(mod 14 -3)
-1
ACL2 !>(mod -14 -3)
-2
ACL2 !>(mod -15 -3)
0
ACL2 !>
```
`(Mod i j)` is that number `k` that `(* j (floor i j))` added to `k` equals `i`.

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

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

## MV

returning multiple values
```Major Section:  PROGRAMMING
```

`Mv` is the mechanism provided by ACL2 for returning two or more values. Logically, `(mv x1 x2 ... xn)` is the same as `(list x1 x2 ... xn)`, a list of the indicated values. However, ACL2 avoids the cost of building this list structure, with the cost that `mv` may only be used in a certain style in definitions: if a function ever returns using `mv` (either directly, or by calling another function that returns multiple values), then this function must always return the same number of multiple values.

For more explanation of the multiple value mechanism, see mv-let.

ACL2 does not support the Common Lisp construct `values`, whose logical meaning seems difficult to characterize. `Mv` is the ACL2 analogue of that construct.

## MV-LET

calling multi-valued ACL2 functions
```Major Section:  PROGRAMMING
```

```Example Form:
(mv-let (x y z)              ; local variables
(mv 1 2 3)           ; multi-valued expression
(declare (ignore y)) ; optional declarations
(cons x z))          ; body
```
The form above binds the three ``local variables,'' `x`, `y`, and `z`, to the three results returned by the multi-valued expression and then evaluates the body. The result is `'(1 . 3)`. The second local, `y`, is declared `ignore`d. The multi-valued expression can be any ACL2 expression that returns `k` results, where `k` is the number of local variables listed. Often however it is simply the application of a `k`-valued function. `Mv-let` is the standard way to invoke a multi-valued function when the caller must manipulate the vector of results returned.

```General Form:
(mv-let (var1 ... vark)
term
body)
or
(mv-let (var1 ... vark)
term
(declare ...) ... (declare ...)
body)
```
where the `vari` are distinct variables, `term` is a term that returns `k` results and mentions only variables bound in the environment containing the `mv-let` expression, and `body` is a term mentioning only the `vari` and variables bound in the environment containing the `mv-let`. Each `vari` must occur in `body` unless it is declared `ignore`d in one of the optional `declare` forms, unless this requirement is turned off; see set-ignore-ok. The value of the `mv-let` term is the result of evaluating `body` in an environment in which the `vari` are bound, in order, to the `k` results obtained by evaluating `term` in the environment containing the `mv-let`.

Here is an extended example that illustrates both the definition of a multi-valued function and the use of `mv-let` to call it. Consider a simple binary tree whose interior nodes are `cons`es and whose leaves are non-`cons`es. Suppose we often need to know the number, `n`, of interior nodes of such a tree; the list, `syms`, of symbols that occur as leaves; and the list, `ints`, of integers that occur as leaves. (Observe that there may be leaves that are neither symbols nor integers.) Using a multi-valued function we can collect all three results in one pass.

Here is the first of two definitions of the desired function. This definition is ``primitive recursive'' in that it has only one argument and that argument is reduced in size on every recursion.

```(defun count-and-collect (x)

; We return three results, (mv n syms ints) as described above.

(cond ((atom x)

; X is a leaf.  Thus, there are 0 interior nodes, and depending on
; whether x is a symbol, an integer, or something else, we return
; the list containing x in as the appropriate result.

(cond ((symbolp x) (mv 0 (list x) nil))
((integerp x)(mv 0 nil      (list x)))
(t           (mv 0 nil      nil))))
(t

; X is an interior node.  First we process the car, binding n1, syms1, and
; ints1 to the answers.

(mv-let (n1 syms1 ints1)
(count-and-collect (car x))

; Next we process the cdr, binding n2, syms2, and ints2.

(mv-let (n2 syms2 ints2)
(count-and-collect (car x))

; Finally, we compute the answer for x from those obtained for its car
; and cdr, remembering to increment the node count by one for x itself.

(mv (1+ (+ n1 n2))
(append syms1 syms2)
(append ints1 ints2)))))))
```
This use of multiple values to ``do several things at once'' is very common in ACL2. However, the function above is inefficient because it appends `syms1` to `syms2` and `ints1` to `ints2`, copying the list structures of `syms1` and `ints1` in the process. By adding ``accumulators'' to the function, we can make the code more efficient.
```(defun count-and-collect1 (x n syms ints)
(cond ((atom x)
(cond ((symbolp x) (mv n (cons x syms) ints))
((integerp x) (mv n syms (cons x ints)))
(t (mv n syms ints))))
(t (mv-let (n2 syms2 ints2)
(count-and-collect1 (cdr x) (1+ n) syms ints)
(count-and-collect1 (car x) n2 syms2 ints2)))))
```
We claim that `(count-and-collect x)` returns the same triple of results as `(count-and-collect1 x 0 nil nil)`. The reader is urged to study this claim until convinced that it is true and that the latter method of computing the results is more efficient. One might try proving the theorem
```(defthm count-and-collect-theorem
(equal (count-and-collect1 x 0 nil nil) (count-and-collect x))).
```
Hint: the inductive proof requires attacking a more general theorem.

ACL2 does not support the Common Lisp construct `multiple-value-bind`, whose logical meaning seems difficult to characterize. `Mv-let` is the ACL2 analogue of that construct.

## MV-NTH

the mv-nth element (zero-based) of a list
```Major Section:  PROGRAMMING
```

`(Mv-nth n l)` is the `n`th element of `l`, zero-based. If `n` is greater than or equal to the length of `l`, then `mv-nth` returns `nil`.

`(Mv-nth n l)` has a guard that `n` is a non-negative integer and `l` is a `true-listp`.

`Mv-nth` is equivalent to the Common Lisp function `nth`, but is used by ACL2 to access the nth value returned by a multiply valued expression. For an example of the use of `mv-nth`, try

```ACL2 !>:trans1 (mv-let (erp val state)
(value (list erp val)))
```

## NFIX

coerce to a natural number
```Major Section:  PROGRAMMING
```

`Nfix` simply returns any natural number argument unchanged, returning `0` on an argument that is not a natural number. Also see ifix, see rfix, see realfix, and see fix for analogous functions that coerce to an integer, a rational number, a real, and a number, respectively.

`Nfix` has a guard of `t`.

## NINTH

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

See any Common Lisp documentation for details.

## NO-DUPLICATESP

check for duplicates in a list (using `eql` for equality)
```Major Section:  PROGRAMMING
```

`(no-duplicatesp l)` is true if and only if no member of `l` occurs twice in `l`.

`(no-duplicatesp l)` has a guard of `(eqlable-listp l)`. Membership is tested using `member`, hence using `eql` as the test.

## NO-DUPLICATESP-EQUAL

check for duplicates in a list (using `equal` for equality)
```Major Section:  PROGRAMMING
```

`(no-duplicatesp-equal l)` is true if and only if no member of `l` occurs twice in `l`.

`(no-duplicatesp-equal l)` has a guard of `(true-listp l)`. Membership is tested using `member-equal`, hence using `equal` as the test.

## NONNEGATIVE-INTEGER-QUOTIENT

natural number division function
```Major Section:  PROGRAMMING
```

```Example Forms:
(nonnegative-integer-quotient 14 3) ; equals 4
(nonnegative-integer-quotient 15 3) ; equals 5
```
`(nonnegative-integer-quotient i j)` returns the integer quotient of the integers `i` and (non-zero) `j`, i.e., the largest `k` such that `(* j k)` is less than or equal to `i`. Also see floor, see ceiling and see truncate, which are derived from this function and apply to rational numbers.

The guard of `(nonnegative-integer-quotient i j)` requires that `i` is a nonnegative integer and `j` is a positive integer.

## NOT

logical negation
```Major Section:  PROGRAMMING
```

`Iff` is the ACL2 negation function. The negation of `nil` is `t` and the negation of anything else is `nil`.

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

## NTH

the nth element (zero-based) of a list
```Major Section:  PROGRAMMING
```

`(Nth n l)` is the `n`th element of `l`, zero-based. If `n` is greater than or equal to the length of `l`, then `nth` returns `nil`.

`(Nth n l)` has a guard that `n` is a non-negative integer and `l` is a `true-listp`.

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

## NTHCDR

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

`(Nthcdr n l)` removes the first `n` elements from the list `l`.

The following is a theorem.

```(implies (and (integerp n)
(<= 0 n)
(true-listp l))
(equal (length (nthcdr n l))
(if (<= n (length l))
(- (length l) n)
0)))
```
For related functions, see take and see butlast.

The guard of `(nthcdr n l)` requires that `n` is a nonnegative integer and `l` is a true list.

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

## NULL

recognizer for the empty list
```Major Section:  PROGRAMMING
```

`Null` is the function that checks whether its argument is `nil`. For recursive definitions it is often preferable to test for the end of a list using `endp` instead of `null`; see endp.

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

## NUMERATOR

dividend of a ratio in lowest terms
```Major Section:  PROGRAMMING
```

Completion Axiom:

```(equal (numerator x)
(if (rationalp x)
(numerator x)
0))
```

Guard for `(numerator x)`:

```(rationalp x)
```

## ODDP

test whether an integer is odd
```Major Section:  PROGRAMMING
```

`(oddp x)` is true if and only if `x` is odd, i.e., not even in the sense of `evenp`.

The guard for `oddp` requires its argument to be an integer.

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

## OR

conjunction
```Major Section:  PROGRAMMING
```

`Or` is the macro for disjunctions. `Or` takes any number of arguments and returns the first that is non-`nil`, or `nil` if there is no non-`nil` element.

`Or` is a Common Lisp macro. See any Common Lisp documentation for more information.

## PAIRLIS

see `pairlis\$`
```Major Section:  PROGRAMMING
```

The Common Lisp language allows its `pairlis` function to construct an alist in any order! So we have to define our own version: See pairlis\$.

## PAIRLIS\$

zipper together two lists
```Major Section:  PROGRAMMING
```

The Common Lisp language allows its `pairlis` function to construct an alist in any order! So we have to define our own version, `pairlis\$`. It returns the list of pairs obtained by `cons`ing together successive respective members of the given lists.

The guard for `pairlis\$` requires that its arguments are true lists.

## PLUSP

test whether a number is positive
```Major Section:  PROGRAMMING
```

`(Plusp x)` is true if and only if `x > 0`.

The guard of `plusp` requires its argument to be a rational (real, in ACL2(r)) number.

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

## POSITION

position of an item in a string or a list, using `eql` as test
```Major Section:  PROGRAMMING
```

`(Position item seq)` is the least index (zero-based) of the element `item` in the string or list `seq`, if in fact `item` is an element of `seq`. Otherwise `(position item seq)` is `nil`.

`(Position item lst)` is provably the same in the ACL2 logic as `(position-equal item lst)`. It has a stronger guard than `position-equal` because uses `eql` to test equality of `item` with members of `lst`. Its guard requires that either `lst` is a string, or else `lst` is a true list such that either `(eqlablep item)` or all members of `lst` are `eqlablep`. See position-equal and see position-eq.

`Position` is a Common Lisp function. See any Common Lisp documentation for more information. Since ACL2 functions cannot take keyword arguments (though macros can), the ACL2 functions `position-equal` and `position-eq` are defined to correspond to calls of the Common Lisp function `position` whose keyword argument `:test` is `equal` or `eq`, respectively.

## POSITION-EQ

position of an item in a string or a list, using `eq` as test
```Major Section:  PROGRAMMING
```

`(Position-eq item seq)` is the least index (zero-based) of the element `item` in the list `seq`, if in fact `item` is an element of `seq`. Otherwise `(position-eq item seq)` is `nil`.

`(Position-eq item lst)` is provably the same in the ACL2 logic as `(position item lst)` and `(position-equal item lst)` when `lst` is a true list, but it has a stronger guard because it uses `eq` for a more efficient test for whether `item` is equal to a given member of `lst`. Its guard requires that `lst` is a true list, and moreover, either `item` is a symbol or `lst` is a list of symbols. See position-equal and see position, which unlike `position-eq` have guards that allow the second argument to be a string.

## POSITION-EQUAL

position of an item in a string or a list
```Major Section:  PROGRAMMING
```

`(Position item seq)` is the least index (zero-based) of the element `item` in the string or list `seq`, if in fact `item` is an element of `seq`. Otherwise `(position item seq)` is `nil`.

`(Position-equal item lst)` has a guard of `(true-listp lst)`. `Position-equal` has the same functionality as the Common Lisp function `position`, except that it uses the `equal` function to test whether `item` is the same as each successive element of `lst`. See position and see position-eq.

## PPROGN

evaluate a sequence of forms that return state
```Major Section:  PROGRAMMING
```

```Example Form:
(pprogn
(cond ((or (equal (car l) #\) (equal (car l) slash-char))
(princ\$ #\ channel state))
(t state))
(princ\$ (car l) channel state)
(mv (cdr l) state))
```
The convention for `pprogn` usage is to give it a non-empty sequence of forms, each of which (except possibly for the last) returns state (see state) as its only value. The state returned by each but the last is passed on to the next. The value or values of the last form are returned as the value of the `pprogn`.

If you are using single-threaded objects you may wish to define an analogue of this function for your own stobj.

General Form:

```(PPROGN form1
form2
...
formk
result-form)
```
This general form is equivalent, via macro expansion, to:
```(LET ((STATE form1))
(LET ((STATE form2))
...
(LET ((STATE formk))
result-form)))
```

## PROG2\$

execute a check before returning a value
```Major Section:  PROGRAMMING
```

See hard-error and see illegal for examples of functions to call in the first argument of `prog2\$`.

Semantically, `(Prog2\$ x y)` equals `y`; the value of `x` is ignored. However, `x` is first evaluated for side effect. Since the ACL2 programming language is applicative, there can be no logical impact of evaluating `x`. However, `x` may involve a call of a function such as `hard-error` or `illegal`, which can cause so-called ``hard errors.''

Here is a simple, contrived example using `hard-error`. The intention is to check at run-time that the input is appropriate before calling function `bar`.

```(defun foo-a (x)
(declare (xargs :guard (consp x)))
(prog2\$
(or (good-car-p (car x))
(hard-error 'foo-a
"Bad value for x: ~p0"
(list (cons #\0 x))))
(bar x)))
```
The following similar function uses `illegal` instead of `hard-error`. Since `illegal` has a guard of `nil`, `guard` verification would guarantee that the call of `illegal` below will never be made (at least when guard checking is on; see set-guard-checking).
```(defun foo-b (x)
(declare (xargs :guard (and (consp x) (good-car-p (car x)))))
(prog2\$
(or (good-car-p (car x))
(illegal 'foo-b
"Bad value for x: ~p0"
(list (cons #\0 x))))
(bar x)))
```

## PROGN

see the documentation for `er-progn`
```Major Section:  PROGRAMMING
```

ACL2 does not allow the use of `progn` in definitions. Instead, a function `er-progn` can be used for sequencing state-oriented operations; see er-progn and see state. If you are using single-threaded objects (see stobj) you may wish to define a version `progn` that cascades the object through successive changes. Our `pprogn` is the `state` analogue of such a macro.

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

## PROOFS-CO

the proofs character output channel
```Major Section:  PROGRAMMING
```

`Proofs-co` is an `ld` special (see ld). The accessor is `(proofs-co state)` and the updater is `(set-proofs-co val state)`. `Proofs-co` must be an open character output channel. It is to this channel that `defun`, `defthm`, and the other event commands print their commentary.

``Proofs-co'' stands for ``proofs character output.'' The initial value of `proofs-co` is the same as the value of `*standard-co*` (see *standard-co*).

## PROPER-CONSP

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

`Proper-consp` is the function that checks whether its argument is a non-empty list that ends in `nil`. Also see true-listp.

## PUT-ASSOC-EQ

modify an association list by associating a value with a key
```Major Section:  PROGRAMMING
```

`(Put-assoc-eq name val alist)` returns an alist that is the same as the list `alist`, except that the first pair in `alist` with a `car` of `name` is replaced by `(cons name val)`, if there is one. If there is no such pair, then `(cons name val)` is added at the end. Note that the order of the keys occurring in `alist` is unchanged (though a new key may be added).

The guard of `(put-assoc-eq name val alist)` requires that `alist` is an `alistp`, and moreover, either `name` is a symbol or `alist` is a `symbol-alistp`.