*

multiplication macro
Major Section:  PROGRAMMING

* is really a macro that expands to calls of the function binary-*. So for example

(* x y 4 z)
represents the same term as
(binary-* x (binary-* y (binary-* 4 z))).

See binary-*.

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













































































*STANDARD-CI*

an ACL2 character-based analogue of CLTL's *standard-input*
Major Section:  PROGRAMMING

The value of the ACL2 constant *standard-ci* is an open character input channel that is synonymous to Common Lisp's *standard-input*.

ACL2 character input from *standard-ci* is actually obtained by reading characters from the stream named by Common Lisp's *standard-input*. That is, by changing the setting of *standard-input* in raw Common Lisp you can change the source from which ACL2 reads on the channel *standard-ci*. See *standard-co*.













































































*STANDARD-CO*

the ACL2 analogue of CLTL's *standard-output*
Major Section:  PROGRAMMING

The value of the ACL2 constant *standard-co* is an open character output channel that is synonymous to Common Lisp's *standard-output*.

ACL2 character output to *standard-co* will go to the stream named by Common Lisp's *standard-output*. That is, by changing the setting of *standard-output* in raw Common Lisp you can change the actual destination of ACL2 output on the channel named by *standard-co*. Observe that this happens without changing the logical value of *standard-co* (which is some channel symbol). Changing the setting of *standard-output* in raw Common Lisp essentially just changes the map that relates ACL2 to the physical world of terminals, files, etc.

To see the value of this observation, consider the following. Suppose you write an ACL2 function which does character output to the constant channel *standard-co*. During testing you see that the output actually goes to your terminal. Can you use the function to output to a file? Yes, if you are willing to do a little work in raw Common Lisp: open a stream to the file in question, set *standard-output* to that stream, call your ACL2 function, and then close the stream and restore *standard-output* to its nominal value. Similar observations can be made about the two ACL2 input channels, *standard-oi* and *standard-ci*, which are analogues of *standard-input*.

Another reason you might have for wanting to change the actual streams associated with *standard-oi* and *standard-co* is to drive the ACL2 top-level loop, ld, on alternative input and output streams. This end can be accomplished easily within ACL2 by either calling ld on the desired channels or file names or by resetting the ACL2 state global variables 'standard-oi and 'standard-co which are used by ld. See standard-oi and see standard-co.













































































*STANDARD-OI*

an ACL2 object-based analogue of CLTL's *standard-input*
Major Section:  PROGRAMMING

The value of the ACL2 constant *standard-oi* is an open object input channel that is synonymous to Common Lisp's *standard-input*.

ACL2 object input from *standard-oi* is actually obtained by reading from the stream named by Common Lisp's *standard-input*. That is, by changing the setting of *standard-input* in raw Common Lisp you can change the source from which ACL2 reads on the channel *standard-oi*. See *standard-co*.













































































+

addition macro
Major Section:  PROGRAMMING

+ is really a macro that expands to calls of the function binary-+. So for example

(+ x y 4 z)
represents the same term as
(binary-+ x (binary-+ y (binary-+ 4 z))).
See binary-+.















































































-

macro for subtraction and negation
Major Section:  PROGRAMMING

See binary-+ for addition and see unary-- for negation.

Note that - represents subtraction as follows:

(- x y)
represents the same term as
(+ x (- y))
which is really
(binary-+ x (unary-- y)).
Also note that - represents arithmetic negation as follows:
(- x)
expands to
(unary-- x).














































































/

macro for division and reciprocal
Major Section:  PROGRAMMING

See binary-* for multiplication and see unary-/ for reciprocal.

Note that / represents division as follows:

(/ x y)
represents the same term as
(* x (/ y))
which is really
(binary-* x (unary-/ y)).
Also note that / represents reciprocal as follows:
(/ x)
expands to
(unary-/ x).
/ is a Common Lisp macro. See any Common Lisp documentation for more information.













































































/=

test inequality of two numbers
Major Section:  PROGRAMMING

(/= x y) is logically equivalent to (not (equal x y)).

Unlike equal, /= has a guard requiring both of its arguments to be numbers. Generally, /= is executed more efficiently than a combination of not and equal.

For a discussion of the various ways to test against 0, See zero-test-idioms.

/= is a Common Lisp function. See any Common Lisp documentation for more information.













































































1+

increment by 1
Major Section:  PROGRAMMING

(1+ x) is the same as (+ 1 x). See +.

1+ is a Common Lisp function. See any Common Lisp documentation for more information.













































































1-

decrement by 1
Major Section:  PROGRAMMING

(1- x) is the same as (- x 1). See -.

1- is a Common Lisp function. See any Common Lisp documentation for more information.













































































<

less-than
Major Section:  PROGRAMMING

Completion Axiom:

(equal (< x y)
       (if (and (rationalp x)
                (rationalp y))
           (< x y)
         (let ((x1 (if (acl2-numberp x) x 0))
               (y1 (if (acl2-numberp y) y 0)))
           (or (< (realpart x1) (realpart y1))
               (and (equal (realpart x1) (realpart y1))
                    (< (imagpart x1) (imagpart y1)))))))

Guard for (< x y):

(and (rationalp x) (rationalp y))
Notice that like all arithmetic functions, < treats non-numeric inputs as 0.

This function has the usual meaning on the rational numbers, but is extended to the complex rational numbers using the lexicographic order: first the real parts are compared, and if they are equal, then the imaginary parts are compared.













































































<=

less-than-or-equal test
Major Section:  PROGRAMMING

<= is a macro, and (<= x y) expands to the same thing as (not (< y x)). See <.

<= is a Common Lisp function. See any Common Lisp documentation for more information.













































































=

test equality (of two numbers, symbols, or characters)
Major Section:  PROGRAMMING

(= x y) is logically equivalent to (equal x y).

Unlike equal, = has a guard requiring both of its arguments to be numbers. Generally, = is executed more efficiently than equal.

For a discussion of the various ways to test against 0, See zero-test-idioms.

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













































































>

greater-than test
Major Section:  PROGRAMMING

> is a macro, and (> x y) expands to the same thing as (< y x). See <.

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













































































>=

greater-than-or-equal test
Major Section:  PROGRAMMING

>= is a macro, and (>= x y) expands to the same thing as (not (< x y)). See <.

>= is a Common Lisp function. See any Common Lisp documentation for more information.













































































ABS

the absolute value of a rational number
Major Section:  PROGRAMMING

(Abs x) is -x if x is negative and is x otherwise.

The guard for abs requires its argument to be a rational numbers.

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

From ``Common Lisp the Language'' page 205, we must not allow complex x as an argument to abs in ACL2, because if we did we would have to return a number that might not be a complex rational number (see complex-rationalp) and hence not an ACL2 object.













































































ACL2-NUMBERP

recognizer for numbers
Major Section:  PROGRAMMING

(acl2-numberp x) is true if and only if x is a number, i.e., a rational or complex rational number.















































































ACL2-USER

a package the ACL2 user may prefer
Major Section:  PROGRAMMING

This package imports the standard Common Lisp symbols that ACL2 supports and also a few symbols from package "ACL2" that are commonly used when interacting with ACL2. You may prefer to select this as your current package so as to avoid colliding with ACL2 system names.

This package imports the symbols listed in *common-lisp-symbols-from-main-lisp-package*, which contains hundreds of CLTL function and macro names including those supported by ACL2 such as cons, car, and cdr. It also imports the symbols in *acl2-exports*, which contains a few symbols that are frequently used while interacting with the ACL2 system, such as implies, defthm, and rewrite. It imports nothing else.

Thus, names such as alistp, member-equal, and type-set, which are defined in the "ACL2" package are not present here. If you find yourself frequently colliding with names that are defined in "ACL2" you might consider selecting "ACL2-USER" as your current package (see in-package). If you select "ACL2-USER" as the current package, you may then simply type member-equal to refer to acl2-user::member-equal, which you may define as you see fit. Of course, should you desire to refer to the "ACL2" version of member-equal, you will have to use the "ACL2::" prefix, e.g., acl2::member-equal.

If, while using "ACL2-USER" as the current package, you find that there are symbols from "ACL2" that you wish we had imported into it (because they are frequently used in interaction), please bring those symbols to our attention. For example, should union-theories and universal-theory be imported? Except for stabilizing on the ``frequently used'' names from "ACL2", we intend never to define a symbol whose symbol-package-name is "ACL2-USER".













































































ACONS

constructor for association lists
Major Section:  PROGRAMMING

(Acons key datum alist) equals the result of consing the pair (cons key datum) to the front of the association list alist.

(Acons key datum alist) has a guard of (alistp alist). Acons is a Common Lisp function. See any Common Lisp documentation for more information.













































































ADD-TO-SET-EQ

add a symbol to a list
Major Section:  PROGRAMMING

For a symbol x and a true list lst, (add-to-set-eq x lst) is the result of consing x on to the front of lst, unless x is already a member of lst, in which case it equals lst.

(add-to-set-eq x lst) has a guard that lst is a true list and moreover, either x is a symbol or lst is a list of symbols.













































































ALISTP

recognizer for association lists
Major Section:  PROGRAMMING

(alistp x) is true if and only if x is a list of cons pairs.

(alistp x) has a guard of t.













































































ALPHA-CHAR-P

recognizer for alphabetic characters
Major Section:  PROGRAMMING

(Alpha-char-p x) is true if and only if x is a alphabetic character, i.e., one of the characters #a, #b, ..., #z, #A, #B, ..., #Z.

The guard for alpha-char-p requires its argument to be a character.

Alpha-char-p is a Common Lisp function. See any Common Lisp documentation for more information.













































































AND

conjunction
Major Section:  PROGRAMMING

And is the macro for conjunctions. And takes any number of arguments. And returns nil if one of the arguments is nil, but otherwise returns the last argument. If there are no arguments, and returns t.

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













































































APPEND

concatenate two or more lists
Major Section:  PROGRAMMING

Append, which takes two or more arguments, expects all the arguments except perhaps the last to be true (null-terminated) lists. It returns the result of concatenating all the elements of all the given lists into a single list. Actually, in ACL2 append is a macro that expands into calls of the binary function binary-append.

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













































































ASH

arithmetic shift operation
Major Section:  PROGRAMMING

(ash i c) is the result of taking the two's complement representation of the integer i and shifting it by c bits, padding with c 0 bits if c is positive, and dropping (abs c) bits if c is negative.

The guard for ash requires that its arguments are integers.

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













































































ASSOC

look up key in association list, using eql as test
Major Section:  PROGRAMMING

(Assoc x alist) is the first member of alist whose car is x, or nil if no such member exists.

(Assoc x alist) is provably the same in the ACL2 logic as (assoc-equal x alist). It has a stronger guard than assoc-equal because it uses eql to test whether x is equal to the car of a given member of alist. Its guard requires that alist is an alistp, and moreover, either (eqlablep x) or all cars of members of alist are eqlablep. See assoc-equal and see assoc-eq.

Assoc 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 assoc-equal and assoc-eq are defined to correspond to calls of the Common Lisp function assoc whose keyword argument :test is equal or eq, respectively.













































































ASSOC-EQ

look up key in association list, using eq as test
Major Section:  PROGRAMMING

(Assoc-eq x alist) is the first member of alist whose car is x, or nil if no such member exists.

(Assoc-eq x alist) is provably the same in the ACL2 logic as (assoc x alist) and (assoc-equal x alist), but it has a stronger guard because it uses eq for a more efficient test for whether x is equal to a given key of alist. Its guard requires that alist is an association list (see alistp), and moreover, either x is a symbol or all keys of alist are symbols, i.e., alist is a symbol-alistp.













































































ASSOC-EQUAL

look up key in association list
Major Section:  PROGRAMMING

(Assoc-equal x alist) is the first member of alist whose car is x, or nil if no such member exists.

(Assoc-equal x alist) has a guard of (alistp alist), and returns the first member of alist whose car is x, or nil if no such member exists. Thus, assoc-equal has the same functionality as the Common Lisp function assoc, except that it uses the equal function to test whether x is the same as each successive `key' of alist. See assoc and see assoc-eq.













































































ASSOC-KEYWORD

look up key in a keyword-value-listp
Major Section:  PROGRAMMING

If l is a list of even length of the form (k1 a1 k2 a2 ... kn an), where each ki is a keyword, then (assoc-keyword key l) is the first tail of l starting with key if key is some ki, and is nil otherwise.

The guard for (assoc-keyword key l) is (keyword-value-listp l).













































































ASSOC-STRING-EQUAL

look up key, a string, in association list
Major Section:  PROGRAMMING

(Assoc-string-equal x alist) is similar to assoc-equal. However, for string x and alist alist, the comparison of x with successive keys in alist is done using string-equal rather than equal.

The guard for assoc-string-equal requires that x is a string and alist is an alist.













































































ATOM

recognizer for atoms
Major Section:  PROGRAMMING

(atom x) is true if and only if x is an atom, i.e., not a cons pair.

Atom has a guard of t, and is a Common Lisp function. See any Common Lisp documentation for more information.













































































ATOM-LISTP

recognizer for a true list of atoms
Major Section:  PROGRAMMING

The predicate atom-listp tests whether its argument is a true-listp of atoms, i.e., of non-conses.















































































BINARY-*

multiplication function
Major Section:  PROGRAMMING

Completion Axiom:

(equal (binary-* x y)
       (if (acl2-numberp x)
           (if (acl2-numberp y)
               (binary-* x y)
             0)
         0))

Guard for (binary-* x y):

(and (acl2-numberp x) (acl2-numberp y))
Notice that like all arithmetic functions, binary-* treats non-numeric inputs as 0.

Calls of the macro * expand to calls of binary-*; see *.













































































BINARY-+

addition function
Major Section:  PROGRAMMING

Completion Axiom:

(equal (binary-+ x y)
       (if (acl2-numberp x)
           (if (acl2-numberp y)
               (binary-+ x y)
             x)
         (if (acl2-numberp y)
             y
           0)))

Guard for (binary-+ x y):

(and (acl2-numberp x) (acl2-numberp y))
Notice that like all arithmetic functions, binary-+ treats non-numeric inputs as 0.

Calls of the macro + expand to calls of binary-+; see +.













































































BINARY-APPEND

concatenate two lists
Major Section:  PROGRAMMING

This binary function implements append, which is a macro in ACL2. See append

The guard for binary-append requires the first argument to be a true-listp.













































































BOOLEANP

recognizer for booleans
Major Section:  PROGRAMMING

(Booleanp x) is t if x is t or nil, and is nil otherwise.

See generalized-booleans for a discussion of a potential soundness problem for ACL2 related to the question: Which Common Lisp functions are known to return Boolean values?













































































BUTLAST

all but a final segment of a list
Major Section:  PROGRAMMING

(Butlast l n) is the list obtained by removing the last n elements from the true list l. The following is a theorem (though it takes some effort, including lemmas, to get ACL2 to prove it).

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

The guard for (butlast l n) requires that n is a nonnegative integer and lst is a true list.

Butlast is a Common Lisp function. See any Common Lisp documentation for more information. Note: In Common Lisp the second argument of butlast is optional, but in ACL2 it is required.













































































CAAAAR

car of the caaar
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CAAADR

car of the caadr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CAAAR

car of the caar
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CAADAR

car of the cadar
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CAADDR

car of the caddr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CAADR

car of the cadr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CAAR

car of the car
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CADAAR

car of the cdaar
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CADADR

car of the cdadr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CADAR

car of the cdar
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CADDAR

car of the cddar
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CADDDR

car of the cdddr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CADDR

car of the cddr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CADR

car of the cdr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CAR

returns the first element of a non-empty list, else nil
Major Section:  PROGRAMMING

Completion Axiom:

(equal (car x)
       (cond
        ((consp x)
         (car x))
        (t nil)))

Guard:

(or (consp x) (equal x nil))
Notice that in the ACL2 logic, car returns nil for every atom.













































































CASE

conditional based on if-then-else using eql
Major Section:  PROGRAMMING

Example Form:
(case typ
  ((:character foo)
   (open file-name :direction :output))
  (bar (open-for-bar file-name))
  (otherwise
   (my-error "Illegal.")))
is the same as
(cond ((member typ '(:character foo))
       (open file-name :direction :output))
      ((eql typ 'bar)
       (open-for-bar file-name))
      (t (my-error "Illegal.")))
which in turn is the same as
(if (member typ '(:character foo))
    (open file-name :direction :output)
    (if (eql typ 'bar)
        (open-for-bar file-name)
        (my-error "Illegal.")))

General Forms: (case expr (x1 val-1) ... (xk val-k) (otherwise val-k+1))

(case expr (x1 val-1) ... (xk val-k) (t val-k+1))

where each xi is either eqlablep or a true list of eqlablep objects.

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













































































CASE-MATCH

pattern matching or destructuring
Major Section:  PROGRAMMING

General Form:
(case-match x
  (pat1 dcl1 body1)
  ...
  (patk dclk bodyk))
where x is a variable symbol, the pati are structural patterns as described below, the dcli are optional declare forms and the bodyi are terms. Return the value(s) of the bodyi corresponding to the first pati matching x, or nil if none matches.

Pattern Language:
With the few special exceptions described below, matching requires that the cons structure of x be isomorphic to that of the pattern, down to the atoms in the pattern. Non-symbol atoms in the pattern match only themselves. Symbols in the pattern denote variables which match anything and which are bound by a successful match to the corresponding substructure of x. Variables that occur more than once must match the same (EQUAL) structure in every occurrence.

Exceptions:
&               Matches anything and is not bound.  Multiple
                  occurrences of & in a pattern may match different
                  structures.
nil, t, *sym*   These symbols cannot be bound and match only their
                  global values.
!sym            where sym is a symbol that is already bound in the
                  context of the case-match, matches only the
                  current binding of sym.
'obj            Matches only itself.
Some examples are shown below.

Below we show some sample patterns and examples of things they match and do not match.

  
pattern       matches         non-matches
(x y y)       (ABC 3 3)       (ABC 3 4)    ; 3 is not 4
(fn x . rst)  (P (A I) B C)   (ABC)        ; NIL is not (x . rst)
              (J (A I))                    ; rst matches nil
('fn (g x) 3) (FN (H 4) 3)    (GN (G X) 3) ; 'fn matches only itself
(& t & !x)    ((A) T (B) (C))              ; provided x is '(C)
Consider the two binary trees that contain three leaves. They might be described as (x . (y . z)) and ((x . y) . z), where x, y, and z are atomic. Suppose we wished to recognize those trees. The following case-match would do:
(case-match tree
  ((x . (y . z))
   (and (atom x) (atom y) (atom z)))
  (((x . y) . z)
   (and (atom x) (atom y) (atom z))))
Suppose we wished to recognize such trees where all three tips are identical. Suppose further we wish to return the tip if the tree is one of those recognized ones and to return the number 7 otherwise.
(case-match tree
  ((x . (x . x))
   (if (atom x) x 7))
  (((x . x) . x)
   (if (atom x) x 7))
  (& 7))
Note that case-match returns nil if no pati matches. Thus if we must return 7 in that case, we have to add as the final pattern the &, which always matches anything.













































































CDAAAR

cdr of the caaar
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDAADR

cdr of the caadr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDAAR

cdr of the caar
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDADAR

cdr of the cadar
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDADDR

cdr of the caddr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDADR

cdr of the cadr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDAR

cdr of the car
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDDAAR

cdr of the cdaar
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDDADR

cdr of the cdadr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDDAR

cdr of the cdar
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDDDAR

cdr of the cddar
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDDDDR

cdr of the cdddr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDDDR

cdr of the cddr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDDR

cdr of the cdr
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































CDR

returns the second element of a cons pair, else nil
Major Section:  PROGRAMMING

Completion Axiom:

(equal (cdr x)
       (cond
        ((consp x)
         (cdr x))
        (t nil)))

Guard:

(or (consp x) (equal x nil))
Notice that in the ACL2 logic, cdr returns nil for every atom.













































































CEILING

division returning an integer by truncating toward positive infinity
Major Section:  PROGRAMMING

Example Forms:
ACL2 !>(ceiling 14 3)
5
ACL2 !>(ceiling -14 3)
-4
ACL2 !>(ceiling 14 -3)
-4
ACL2 !>(ceiling -14 -3)
5
ACL2 !>(ceiling -15 -3)
5
(Ceiling i j) is the result of taking the quotient of i and j and returning the smallest integer that is at least as great as that quotient. For example, the quotient of -14 by 3 is -4 2/3, and the smallest integer at least that great is -4.

The guard for (ceiling i j) requires that i and j are rational numbers and j is non-zero.

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













































































CHAR

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

(Char s n) is the nth element of s, zero-based. If n is greater than or equal to the length of s, then char returns nil.

(Char s n) has a guard that n is a non-negative integer and s is a stringp.

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













































































CHAR-CODE

the numeric code for a given character
Major Section:  PROGRAMMING

Completion Axiom:

(equal (char-code x)
       (if (characterp x)
           (char-code x)
         0))

Guard for (char-code x):

(characterp x)
This function maps all non-characters to 0.













































































CHAR-DOWNCASE

turn upper-case characters into lower-case characters
Major Section:  PROGRAMMING

(Char-downcase x) is equal to #A when x is #a, #B when x is #b, ..., and #Z when x is #z, and is x for any other character.

The guard for char-downcase requires its argument to be a character.

Char-downcase is a Common Lisp function. See any Common Lisp documentation for more information.













































































CHAR-EQUAL

character equality without regard to case
Major Section:  PROGRAMMING

For characters x and y, (char-equal x y) is true if and only if x and y are the same except perhaps for their case.

The guard on char-equal requires that its arguments are both characters.

Char-equal is a Common Lisp function. See any Common Lisp documentation for more information.













































































CHAR-UPCASE

turn lower-case characters into upper-case characters
Major Section:  PROGRAMMING

(Char-upcase x) is equal to #A when x is #a, #B when x is #b, ..., and #Z when x is #z, and is x for any other character.

The guard for char-upcase requires its argument to be a character.

Char-upcase is a Common Lisp function. See any Common Lisp documentation for more information.