This is documentation for ACL2 Version 3.3
Copyright (C) 2007  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

CDAADR    cdr of the caadr

See any Common Lisp documentation for details.

CDAAR    cdr of the caar

See any Common Lisp documentation for details.

CDADAR    cdr of the cadar

See any Common Lisp documentation for details.

CDADDR    cdr of the caddr

See any Common Lisp documentation for details.

CDADR    cdr of the cadr

See any Common Lisp documentation for details.

CDAR    cdr of the car

See any Common Lisp documentation for details.

CDDAAR    cdr of the cdaar

See any Common Lisp documentation for details.

CDDADR    cdr of the cdadr

See any Common Lisp documentation for details.

CDDAR    cdr of the cdar

See any Common Lisp documentation for details.

CDDDAR    cdr of the cddar

See any Common Lisp documentation for details.

CDDDDR    cdr of the cdddr

See any Common Lisp documentation for details.

CDDDR    cdr of the cddr

See any Common Lisp documentation for details.

CDDR    cdr of the cdr

See any Common Lisp documentation for details.

CDR    returns the second element of a cons pair, else nil

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

     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 (real,
in ACL2(r)) numbers and j is non-zero.

Ceiling is a Common Lisp function.  See any Common Lisp documentation
for more information.  However, note that unlike Common Lisp, the ACL2
ceiling function returns only a single value,

CHAR    the nth element (zero-based) of a string

(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

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

(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 standard
character (see STANDARD-CHAR-P).

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

CHAR-EQUAL    character equality without regard to case

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 standard
characters (see STANDARD-CHAR-P).

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

(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 standard
character (see STANDARD-CHAR-P).

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

CHAR<    less-than test for characters

(char< x y) is true if and only if the character code of x is less than
that of y.  See CHAR-CODE.

The guard for char< specifies that its arguments are characters.

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

CHAR<=    less-than-or-equal test for characters

(char<= x y) is true if and only if the character code of x is less
than or equal to that of y.  See CHAR-CODE.

The guard for char<= specifies that its arguments are characters.

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

CHAR>    greater-than test for characters

(char> x y) is true if and only if the character code of x is greater
than that of y.  See CHAR-CODE.

The guard for char> specifies that its arguments are characters.

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

CHAR>=    greater-than-or-equal test for characters

(char>= x y) is true if and only if the character code of x is greater
than or equal to that of y.  See CHAR-CODE.

The guard for char>= specifies that its arguments are characters.

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

CHARACTER-ALISTP    recognizer for association lists with characters as keys

(Character-alistp x) is true if and only if x is a list of pairs of the
form (cons key val) where key is a characterp.

CHARACTER-LISTP    recognizer for a true list of characters

The predicate character-listp tests whether its argument is a true list
of characters.

CHARACTERP    recognizer for characters

(characterp x) is true if and only if x is a character.

CHARACTERS    characters in ACL2

ACL2 accepts 256 distinct characters, which are the characters obtained
by applying the function code-char to each integer from 0 to 255.
Among these, Common Lisp designates certain ones as _standard
characters_, namely those of the form (code-char n) where n is from 33
to 126, together with #\Newline and #\Space.  The actual standard
characters may be viewed by evaluating the defconst *standard-chars*.

To be more precise, Common Lisp does not specify the precise
relationship between code-char and the standard characters.  However,
we check that the underlying Common Lisp implementation uses a
particular relationship that extends the usual ASCII coding of
characters.  We also check that Space, Tab, Newline, Page, and Rubout
correspond to characters with respective char-codes 32, 9, 10, 12, and
127.

Code-char has an inverse, char-code.  Thus, when char-code is applied
to an ACL2 character, c, it returns a number n between 0 and 255
inclusive such that (code-char n) = c.

The preceding paragraph implies that there is only one ACL2 character
with a given character code.  CLTL allows for "attributes" for
characters, which could allow distinct characters with the same code,
but ACL2 does not allow this.

_The Character Reader_

ACL2 supports the `#\' notation for characters provided by Common Lisp,
with some restrictions.  First of all, for every character c, the
notation

     #\c

may be used to denote the character object c.  That is, the user may
type in this notation and ACL2 will read it as denoting the character
object c.  In this case, the character immediately following c must be
one of the following "terminating characters": a Tab, a Newline, a Page
character, a space, or one of the characters:

     "  '  (  )  ;  `  ,

Other than the notation above, ACL2 accepts alternate notation for five
characters.

     #\Space
     #\Tab
     #\Newline
     #\Page
     #\Rubout

Again, in each of these cases the next character must be from among the
set of "terminating characters" described in the single-character case.
Our implementation is consistent with IS0-8859, even though we don't
provide #\ syntax for entering characters other than that described
above.

Finally, we note that it is our intention that any object printed by
ACL2's top-level-loop may be read back into ACL2.  Please notify the
implementors if you find a counterexample to this claim.

CLOSE-INPUT-CHANNEL    See IO.

CLOSE-OUTPUT-CHANNEL    See IO.

CODE-CHAR    the character corresponding to a given numeric code

Completion Axiom:

     (equal (code-char x)
            (if (and (integerp x)
                     (>= x 0)
                     (< x 256))
                (code-char x)
              (code-char 0)))

Guard for (code-char x):

     (and (integerp x)
          (>= x 0)
          (< x 256))

ACL2 supports 8-bit characters.  Inputs not between 0 and 255 are
treated as 0.

COERCE    coerce a character list to a string and a string to a list

Completion Axiom:

     (equal (coerce x y)
            (cond
             ((equal y 'list)
              (if (stringp x)
                  (coerce x 'list)
                nil))
             (t
              (coerce (make-character-list x) 'string))))

Guard for (coerce x y):

     (if (equal y 'list)
         (stringp x)
       (if (equal y 'string)
           (character-listp x)
         nil))

COMPILATION    compiling ACL2 functions

ACL2 has several mechanisms to speed up the evaluation of function
calls by _compiling_ functions: see COMP, see
SET-COMPILE-FNS, and see CERTIFY-BOOK.  The intention is that
compilation never changes the value returned by a function call, though
it could cause the call to succeed rather than fail, for example by
avoiding a stack overflow.

The state global variable 'suppress-compile is set automatically when
the system is built, according to the underlying Lisp implementation.  A
non-nil value of this variable -- that is, a nonnil value of (@
suppress-compile) -- avoids all explicit calls to the compiler:
include-book and certify-book coerce their compilation arguments to
nil, and both comp and set-compile-fns are no-ops.  When this is the
case, it is because our experience is that performance on the given
platform when explicit compilation is suppressed may be slightly better
than when the compiler is invoked explicitly.  For example, this
situation is the case when the underlying Lisp is OpenMCL.  A key is
that OpenMCL compiles on-the-fly even when the compiler is not called
explicitly, and compiling a file in OpenMCL (at least as of early 2007)
does not seem to improve appreciably the efficiency of the generated
code.

COMPLEX    create an ACL2 number

     Examples:
     (complex x 3) ; x + 3i, where i is the principal square root of -1
     (complex x y) ; x + yi
     (complex x 0) ; same as x, for rational numbers x

The function complex takes two rational number arguments and returns an
ACL2 number.  This number will be of type (complex rational) [as
defined in the Common Lisp language], except that if the second
argument is zero, then complex returns its first argument.  The
function complex-rationalp is a recognizer for complex rational
numbers, i.e. for ACL2 numbers that are not rational numbers.

The reader macro #C (which is the same as #c) provides a convenient way
for typing in complex numbers.  For explicit rational numbers x and y,
#C(x y) is read to the same value as (complex x y).

The functions realpart and imagpart return the real and imaginary parts
(respectively) of a complex (possibly rational) number.  So for
example, (realpart #C(3 4)) = 3, (imagpart #C(3 4)) = 4, (realpart 3/4)
= 3/4, and (imagpart 3/4) = 0.

The following built-in axiom may be useful for reasoning about complex
numbers.

     (defaxiom complex-definition
       (implies (and (real/rationalp x)
                     (real/rationalp y))
                (equal (complex x y)
                       (+ x (* #c(0 1) y))))
       :rule-classes nil)

A completion axiom that shows what complex returns on arguments
violating its guard (which says that both arguments are rational
numbers) is the following.

     (equal (complex x y)
            (complex (if (rationalp x) x 0)
                     (if (rationalp y) y 0)))

COMPLEX-RATIONALP    recognizes complex rational numbers

     Examples:
     (complex-rationalp 3)       ; nil, as 3 is rational, not complex rational
     (complex-rationalp #c(3 0)) ; nil, since #c(3 0) is the same as 3
     (complex-rationalp t)       ; nil
     (complex-rationalp #c(3 1)) ; t, as #c(3 1) is the complex number 3 + i

See COMPLEX for more about complex rationals in ACL2.

COMPLEX/COMPLEX-RATIONALP    recognizer for complex numbers

For most ACL2 users, this is a macro abbreviating complex-rationalp;
see COMPLEX-RATIONALP.  In  ACL2(r) (see REAL), a
complex number x may have irrational real and imaginary parts.  This
macro abbreviates the predicate complexp in ACL2(r), which holds for
such x.  Most ACL2 users can ignore this macro and use complex-rationalp
instead.  Some books in the ACL2 distribution use
complex/complex-rationalp so that they are suitable for ACL2(r) as well.

CONCATENATE    concatenate lists or strings together

     Examples:
     (concatenate 'string "ab" "cd" "ef")     ; equals "abcdef"
     (concatenate 'string "ab")               ; equals "ab"
     (concatenate 'list '(a b) '(c d) '(e f)) ; equals '(a b c d e f)
     (concatenate 'list)                      ; equals nil

     General Form:
     (concatenate result-type x1 x2 ... xn)

where n >= 0 and either:  result-type is 'string and each xi is a
string; or result-type is 'list and each xi is a true list.
Concatenate simply concatenates its arguments to form the result string
or list.  Also see APPEND and see STRING-APPEND, though
concatenate is probably preferable to string-append for efficiency.

Note:  We do *not* try to comply with the Lisp language's insistence
that concatenate copies its arguments.  Not only are we in an
applicative setting, where this issue shouldn't matter for the logic,
but also we do not actually modify the underlying lisp implementation
of concatenate; we merely provide a definition for it.

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

COND    conditional based on if-then-else

Cond is the construct for IF, THEN, ELSE IF, ...  The test is against
nil.  The argument list for cond is a list of "clauses", each of which
is a list.  In ACL2, clauses must have length 1 or 2.

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

CONJUGATE    complex number conjugate

Conjugate takes an ACL2 number as an argument, and returns its complex
conjugate (i.e., the result of negating its imaginary part.).

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

CONS    pair and list constructor

(cons x y) is a pair whose first component is x and second component is
y.  If y is a list, then (cons x y) is a list that has an addtional
element x on the front.

CONSP    recognizer for cons pairs

(consp x) is true if and only if x is a cons pair.

CW    print to the comment window

Example:

     (cw "The goal is ~p0 and the alist is ~x1.~%"
         (untranslate term t nil)
         unify-subst)

Logically, this expression is equivalent to nil.  However, it has the
effect of first printing to the so-called "comment window" the fmt
string as indicated.  Thus, cw is like fmt (see FMT) except in
three important ways.  First, it is a :logic mode function.  Second, it
neither takes nor returns the ACL2 state;  logically cw simply returns
nil, although it prints to a _comment window_ that just happens to
share the terminal screen with the standard character output
*standard-co*.  Third, its fmt args are positional references, so that
for example

     (cw "Answers: ~p0 and ~p1" ans1 ans2)

prints in the same manner as:

     (fmt "Answers: ~p0 and ~p1"
          (list (cons #\0 ans1) (cons #\1 ans2))
          *standard-co* state nil)

Typically, calls of cw are embedded in prog2$ forms, e.g.,

     (prog2$ (cw ...)
             (mv a b c))

which has the side-effect of printing to the comment window and
logically returning (mv a b c).

     General Form:
     (cw fmt-string arg1 arg2 ... argn)

where n is between 0 and 9 (inclusive).  The macro uses
fmt-to-comment-window, passing it the column 0 and evisc-tuple nil,
after assembling the appropriate alist binding the fmt vars #\0 through
#\9; see FMT.  If you want

     (a) more than 10 vars,
     (b) vars other than the digit chars,
     (c) a different column, or
     (d) a different evisc-tuple,

then call fmt-to-comment-window instead.

Also see CW!, which is useful if you want to be able to read
the printed forms back in.

CW!    print to the comment window

This is the same as cw, except that cw inserts backslash (\) characters
when forced to print past the right margin, in order to make the output
a bit clearer in that case.  Use cw! instead if you want to be able to
read the forms back in.

DECLARE    declarations

     Examples:
     (declare (ignore x y z))
     (declare (ignorable x y z)
              (type integer i j k)
              (type (satisfies integerp) m1 m2))
     (declare (xargs :guard (and (integerp i)
                                 (<= 0 i))
                     :guard-hints (("Goal" :use (:instance lemma3
                                                   (x (+ i j)))))))

     General Form:
     (declare d1 ... dn)
     where, in ACL2, each di is of one of the following forms:

       (ignore v1 ... vn) -- where each vi is a variable introduced in
       the immediately superior lexical environment.  These variables must not
       occur free in the scope of the declaration.

       (ignorable v1 ... vn) -- where each vi is a variable introduced in
       the immediately superior lexical environment.  These variables need not
       occur free in the scope of the declaration.  This declaration can be useful
       for inhibiting compiler warnings.

       (type type-spec v1 ... vn) -- where each vi is a variable introduced in the
       immediately superior lexical environment and type-spec is a type specifier
       (as described in the documentation for type-spec).

       (xargs :key1 val1 ... :keyn valn) -- where the legal values of the keyi's
       and their respective vali's are described in the documentation for
       xargs.

Declarations in ACL2 may occur only where dcl occurs below:

       (DEFUN name args doc-string dcl ... dcl body)
       (DEFMACRO name args doc-string dcl ... dcl body)
       (LET ((v1 t1) ...) dcl ... dcl body)
       (MV-LET (v1 ...) term dcl ... dcl body)

Of course, if a form macroexpands into one of these (as let* expands
into nested lets and our er-let* expands into nested mv-lets) then
declarations are permitted as handled by the macros involved.

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

DEFN    definition with guard t

Defn is defun with guard t.

DENOMINATOR    divisor of a ratio in lowest terms

Completion Axiom:

     (equal (denominator x)
            (if (rationalp x)
                (denominator x)
              1))

Guard for (denominator x):

     (rationalp x)

DIGIT-CHAR-P    the number, if any, corresponding to a given character

(digit-char-p ch) is the integer corresponding to the character ch in
base 10.  For example, (digit-char-p #\3) is equal to the integer 3.
More generally, an optional second argument specifies the radix
(default 10, as indicated above).

The guard for digit-char-p (more precisely, for the function
our-digit-char-p that calls of this macro expand to) requires its
second argument to be an integer between 2 and 36, inclusive, and its
first argument to be a character.

Digit-char-p is a Common Lisp function, though it is implemented in the
ACL2 logic as an ACL2 macro.  See any Common Lisp documentation for
more information.

DIGIT-TO-CHAR    map a digit to a character

     Example:
     ACL2 !>(digit-to-char 8)
     #\8

For an integer n from 0 to 15, (digit-to-char n) is the character
corresponding to n in hex notation, using uppercase letters for digits
exceeding 9.  If n is in the appropriate range, that result is of course
also the binary, octal, and decimal digit.

The guard for digit-to-char requires its argument to be an integer
between 0 and 9, inclusive.

E0-ORD-<    the old ordering function for ACL2 ordinals

See O< for the current new ordering function for ACL2 ordinals.

The functions e0-ordinalp and e0-ord-< were replaced in ACL2
Version_2.8 by o-p and o<, respectively.  However, books created before
that version used the earlier functions for termination proofs; the old
functions might be of use in these cases.  To use the old functions in
termination proofs, include the book books/ordinals/e0-ordinal and
execute the event (set-well-founded-relation e0-ord-<) (see
SET-WELL-FOUNDED-RELATION).  For a more thorough discussion of these
functions, see the documentation at the end of
books/ordinals/e0-ordinal.lisp.

E0-ORDINALP    the old recognizer for ACL2 ordinals

See O-P for the current recognizer for ACL2 ordinals.

The functions e0-ordinalp and e0-ord-< were replaced in ACL2
Version_2.8 by o-p and o<, respectively.  However, books created before
that version used the earlier functions for termination proofs; the old
functions might be of use in these cases.  To use the old functions in
termination proofs, include the book books/ordinals/e0-ordinal and
execute the event (set-well-founded-relation e0-ord-<) (see
SET-WELL-FOUNDED-RELATION).  For a more thorough discussion of these
functions, see the documentation at the end of
books/ordinals/e0-ordinal.lisp.

EIGHTH    eighth member of the list

See any Common Lisp documentation for details.

ENDP    recognizer for empty lists

In the ACL2 logic, (endp x) is the same as (atom x).  See ATOM.

Unlike atom, the guard for endp requires that x is a cons pair or is
nil.  Thus, endp is typically used as a termination test for functions
that recur on a true-listp argument.  See GUARD for general
information about guards.

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

EQ    equality of symbols

Eq is the function for determining whether two objects are identical
(i.e., have the exact same store address in the current von Neumann
implementation of Common Lisp).  It is the same as equal in the ACL2
logic.

Eq is a Common Lisp function.  In order to ensure conformance with
Common Lisp, the ACL2 guard on eq requires at least one of the
arguments to eq to be a symbol.  Common Lisp guarantees that if x is a
symbol, then x is eq to y if and only if x is equal to y.  Thus, the
ACL2 user should think of eq as nothing besides a fast means for
checking equal when one argument is known to be a symbol.  In
particular, it is possible that an eq test will not even require the
cost of a function call but will be as fast as a single machine
instruction.

EQL    test equality (of two numbers, symbols, or characters)

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

Unlike equal, eql has a guard requiring at least one of its arguments
to be a number, a symbol, or a character.  Generally, eql is executed
more efficiently than equal.

For a discussion of the various ways to test against 0, See
ZERO-TEST-IDIOMS.

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

EQLABLE-ALISTP    recognizer for a true list of pairs whose cars are suitable for eql

The predicate eqlable-alistp tests whether its argument is a true-listp
of consp objects whose cars all satisfy eqlablep.

EQLABLE-LISTP    recognizer for a true list of objects each suitable for eql

The predicate eqlable-listp tests whether its argument is a true-listp
of objects satisfying eqlablep.

EQLABLEP    the guard for the function eql

The predicate eqlablep tests whether its argument is suitable for eql,
at least one of whose arguments must satisfy this predicate in Common
Lisp.  (Eqlablep x) is true if and only if its argument is a number, a
symbol, or a character.

EQUAL    true equality

(equal x y) is equal to t or nil, according to whether or not x and y
are the same value.

For a discussion of the various idioms for testing against 0, See
ZERO-TEST-IDIOMS.

ER    print an error message and ``cause an error''

     Example Forms:
     (er hard  'top-level "Illegal inputs, ~x0 and ~x1." a b)
     (er hard? 'top-level "Illegal inputs, ~x0 and ~x1." a b)
     (er soft  'top-level "Illegal inputs, ~x0 and ~x1." a b)

The examples above all print an error message to standard output saying
that a and b are illegal inputs.  However, the first two abort
evaluation after printing an error message, while the third returns (mv
t nil state) after printing an error message.  The result in the third
case can be interpreted as an "error" when programming with the ACL2
state, something most ACL2 users will probably not want to do; see
LD-ERROR-TRIPLES and see ER-PROGN.

Er is a macro, and the above three examples expand to calls of ACL2
functions, as shown below.  See ILLEGAL, see
HARD-ERROR, and see ERROR1, respectively.

     General forms:
     (er hard  ctx fmt-string arg1 arg2 ... argk)
       ==> {macroexpands, in essence, to:}
     (ILLEGAL    CTX FMT-STRING
                 (LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))

     (er hard? ctx fmt-string arg1 arg2 ... argk)
       ==> {macroexpands, in essence, to:}
     (HARD-ERROR CTX FMT-STRING
                 (LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))

     (er soft  ctx fmt-string arg1 arg2 ... argk)
       ==> {macroexpands, in essence, to:}
     (ERROR1     CTX FMT-STRING
                 (LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))

ER-PROGN    perform a sequence of state-changing ``error triples''

     Example:
     (er-progn (check-good-foo-p (f-get-global 'my-foo state) state)
               (value (* (f-get-global 'my-foo state)
                         (f-get-global 'bar state))))

This sequencing primitive is only useful when programming with state,
something that very few users will probably want to do.  See
STATE.

Er-progn is used much the way that progn is used in Common Lisp, except
that it expects each form within it to evaluate to an "error triple" of
the form (mv erp val state).  The first such form, if any, that
evaluates to such a triple where erp is not nil yields the error triple
returned by the er-progn.  If there is no such form, then the last form
returns the value of the er-progn form.

We intend to write more about this topic, especially if there are
requests to do so.

ERROR1    print an error message and cause a ``soft error''

(Error1 ctx str alist) returns (mv t nil state).  An error message is
first printed using the the "context" ctx, as well as the string str
and alist alist that are of the same kind as expected by fmt.  See
FMT.

Error1 can be interpreted as causing an "error" when programming with
the ACL2 state, something most ACL2 users will probably not want to do;
see LD-ERROR-TRIPLES and see ER-PROGN.  In order to
cause errors with :logic mode functions, see HARD-ERROR and see
ILLEGAL.  Better yet, see ER for a macro that provides
a unified way of signaling errors.

As mentioned above, error1 always returns (mv t nil state).  But if a
call (error1 ctx str alist) is encountered during evaluation, then the
string str is first printed using the association list alist (as in
fmt).  Here is a trivial, contrived example.

     ACL2 !>(error1 'my-context
                    "Printing 4: ~n0"
                    (list (cons #\0 4))
                    state)

     ACL2 Error in MY-CONTEXT:  Printing 4: four

     ACL2 !>

EVENP    test whether an integer is even

(evenp x) is true if and only if the integer x is even.  Actually, in
the ACL2 logic (evenp x) is defined to be true when x/2 is an integer.

The guard for evenp requires its argument to be an integer.

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

EXPLODE-NONNEGATIVE-INTEGER    the list of characters in the radix-r form of a number

     Examples:
     ACL2 !>(explode-nonnegative-integer 925 10 nil)
     (#9 #2 #5)
     ACL2 !>(explode-nonnegative-integer 325 16 nil)
     (#3 #9 #D)

For a non-negative integer n, (explode-nonnegative-integer n r nil) is
the list of characters in the radix-r (base-r) representation of n.

The guard for explode-nonnegative-integer requires the first argument
to be a nonnegative integer and second argument to be a valid radix for
ACL2 (2, 8, 10, or 16).

EXPT    exponential function

(Expt r i) is the result of raising the number r to the integer power i.

The guard for (expt r i) is that r is a number and i is an integer, and
furthermore, if r is 0 then i is nonnegative.  When the type
requirements of the guard aren't met, (expt r i) first coerces r to a
number and i to an integer.

Expt is a Common Lisp function.  See any Common Lisp documentation for
more information.  Note that r can be a complex number; this is
consistent with Common lisp.

FIFTH    fifth member of the list

See any Common Lisp documentation for details.

FIRST    first member of the list

See any Common Lisp documentation for details.

FIX    coerce to a number

Fix simply returns any numeric argument unchanged, returning 0 on a
non-numeric argument.  Also see NFIX, see IFIX, and see
RFIX for analogous functions that coerce to a natural number,
an integer, and a rational number, respectively.

Fix has a guard of t.

FIX-TRUE-LIST    coerce to a true list

Fix-true-list is the identity function on true-listp objects.  It
converts every list to a true list by dropping the final cdr, and it
converts every atom to nil.

FLET    local binding of function symbols

     Example Form:
     ; The following evaluates to (mv 7 10):
     (flet ((f (x)
               (+ x 3))
            (g (x)
               (declare (type integer x))
               (* x 2)))
       (mv (f 4) (g 5)))

     General Form:
     (flet (def1 ... defk) body)

where body is a term, and each defi is a definition as in defun but
with the leading defun symbol omitted.  See DEFUN.  The
innermost flet-binding of a function symbol, f, above a call of f, is
the one that provides the definition of f for that call.  Note that
flet does not provide recursion.  Consider the following example.

     (defun f (x) (+ x 3))
     (flet ((f (x) (cons x (f (1+ x)))))
       (f 4))

In the above term (cons x (f (1+ x))), f refers to the global
definition of f above the flet expression.  However, (f 4) refers to
the flet-binding of f, (f (x) (cons x (f x))).  The result of the flet
expression is thus obtained by evaluating (f 4) where (f 4) is (cons 4
(f (1+ 4))), where the latter call of f refers to the global
definition; thus we have (cons 4 (f 5)), which evaluates to (4 . 8).

Although flet behaves in ACL2 essentially as it does in Common Lisp,
ACL2 imposes the following restrictions and qualifications.

     o Every declare form for a local definition (def1 through defk,
     above) must be an ignore, ignorable, or type expression.

     o Each defi must bind a different function symbol.

     o Each defi must bind a symbol that is a legal name for an ACL2
     function symbol.  In particular, the symbol may not be in the
     keyword package or the main Lisp package.  Moreover, the symbol
     may not be a built-in ACL2 function or macro.

     o Every variable occurring in the body of a defi must be a formal
     parameter of that defi.  (This restriction is not enforced in
     Common Lisp.  If the restriction is inconvenient for you, the ACL2
     implementors may be able to remove it, with some effort, if you
     ask.)

     o If the flet-binding defi is in the body of a function f, then
     the stobj inputs for defi are implicitly those of its inputs that
     are declared stobj inputs of f.

Flet bindings are evaluated in parallel.  Consider the following
example.

     (defun f (x) x)
     (flet ((f (x) (cons x x))
            (g (x) (f x)))
       (g 3))

The binding of g refers to the global value of f, not the flet-binding
of f.  Thus, the flet expression evaluates to 3.  Compare the flet
expression above to the following one, which instead evaluates to (3 .
3).

     (defun f (x) x)
     (flet ((f (x) (cons x x)))
       (flet ((g (x) (f x)))
         (g 3)))

Under the hood, ACL2 translates flet bindings to lambda expressions
(see TERM).  The following example illustrates this point.

     ACL2 !>:trans (flet ((f (x) (cons x x))
                          (g (x y) (+ x y)))
                     (f (g 3 4)))

     ((LAMBDA (X) (CONS X X))
      ((LAMBDA (X Y) (BINARY-+ X Y)) '3 '4))

     => *

     ACL2 !>

Flet is part of Common Lisp.  See any Common Lisp documentation for
more information.

FLOOR    division returning an integer by truncating toward negative infinity

     Example Forms:
     ACL2 !>(floor 14 3)
     4
     ACL2 !>(floor -14 3)
     -5
     ACL2 !>(floor 14 -3)
     -5
     ACL2 !>(floor -14 -3)
     4
     ACL2 !>(floor -15 -3)
     5

(Floor i j) returns the result of taking the quotient of i and j and
returning the greatest integer not exceeding that quotient.  For
example, the quotient of -14 by 3 is -4 2/3, and the largest integer
not exceeding that rational number is -5.

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

Floor is a Common Lisp function.  See any Common Lisp documentation for
more information.  However, note that unlike Common Lisp, the ACL2
floor function returns only a single value,

FMS    :(str alist co-channel state evisc) => state

See FMT for further explanation, including documentation of the
tilde-directives.

FMS!    :(str alist co-channel state evisc) => state

This function is nearly identical to fms; see FMS.  The only
difference is that fms may insert backslash (\) characters when forced
to print past the right margin in order to make the output a bit
clearer in that case.  Use fms! instead if you want to be able to read
the forms back in.