Info file: acl2-doc-lemacs.info, -*-Text-*- produced by `texinfo-format-buffer' from file `acl2-doc-lemacs.texinfo' using `texinfmt.el' version 2.32 of 19 November 1993. This is documentation for ACL2 Version 1.8 Copyright (C) 1989-95 Computational Logic, Inc. (CLI). All rights reserved.  File: acl2-doc-lemacs.info, Node: PROPS, Next: Q, Prev: LD, Up: OTHER PROPS print the ACL2 properties on a symbol Example: :props assoc-eq Props takes one argument, a symbol, and prints all of the properties that are on that symbol in the ACL2 world.  File: acl2-doc-lemacs.info, Node: Q, Next: REBUILD, Prev: PROPS, Up: OTHER Q quit ACL2 (type :q) -- reenter with (lp) Example: ACL2 !>:Q The keyword command :q typed at the top-level of the ACL2 loop will terminate the loop and return control to the Common Lisp top-level (or, more precisely, to whatever program invoked lp). To reenter the ACL2 loop, execute (acl2::lp) in Common Lisp. You will be in the same state as you were when you exited with :q, unless during your stay in Common Lisp you messed the data structures representating the ACL2 state. Unlike all other keyword commands, typing :q is not equivalent to invoking the function q. There is no function q.  File: acl2-doc-lemacs.info, Node: REBUILD, Next: RESET-LD-SPECIALS, Prev: Q, Up: OTHER REBUILD a convenient way to reconstruct your old state Examples: ACL2 !>(rebuild "project.lisp") ACL2 !>(rebuild "project.lisp" t) ACL2 !>(rebuild "project.lisp" :all) ACL2 !>(rebuild "project.lisp" :query) ACL2 !>(rebuild "project.lisp" 'lemma-22) Rebuild allows you to assume all the commands in a given file or list, supplied in the first argument. Because rebuild processes an arbitrary sequence of commands with ld-skip-proofsp t, it is unsound! However, if each of these commands is in fact admissible, then processing them with rebuild will construct the same logical state that you would be in if you typed each command and waited through the proofs again. Thus, rebuild is a way to reconstruct a state previously obtained by proving your way through the commands. The second, optional argument to rebuild is a "filter" (*Note LD-PRE-EVAL-FILTER::) that lets you specify which commands to process. You may specify t, :all, :query, or a new logical name. t and :all both mean that you expect the entire file or list to be processed. :query means that you will be asked about each command in turn. A new name means that all commands will be processed as long as the name is new, i.e., rebuild will stop processing commands immediately after executing a command that introduces name. Rebuild will also stop if any command causes an error. You may therefore wish to plant an erroneous form in the file, e.g., (mv t nil state), (*Note LD-ERROR-TRIPLES::), to cause rebuild to stop there. The form (i-am-here) is such a pre-defined form. If you do not specify a filter, rebuild will query you for one. Inspection of the definition of rebuild, e.g., via :pc rebuild-fn, will reveal that it is just a glorified call to the function ld. *Note LD:: if you find yourself wishing that rebuild had additional functionality.  File: acl2-doc-lemacs.info, Node: RESET-LD-SPECIALS, Next: SET-GUARD-CHECKING, Prev: REBUILD, Up: OTHER RESET-LD-SPECIALS restores initial settings of the ld specials Examples: (reset-ld-specials t) (reset-ld-specials nil) Roughly speaking, the ld specials are certain state global variables, such as current-package, ld-prompt, and ld-pre-eval-filter, which are managed by ld as though they were local variables. These variables determine the channels on which ld reads and prints and control many options of ld. *Note LD:: for the details on what the ld specials are. This function, reset-ld-specials, takes one Boolean argument, flg. The function resets all of the ld specials to their initial, top-level values, except for the three channel variables, standard-oi, standard-co, and proofs-co, which are reset to their initial values only if flg is non-nil. Of course, if you are in a recursive call of ld, then when you exit that call, the ld specials will be restored to the values they had at the time ld was called recursively. To see what the initial values are, inspect the value of the constant *initial-ld-special-bindings*.  File: acl2-doc-lemacs.info, Node: SET-GUARD-CHECKING, Next: SET-INHIBIT-OUTPUT-LST, Prev: RESET-LD-SPECIALS, Up: OTHER SET-GUARD-CHECKING control checking guards during execution of top-level forms The top-level ACL2 loop has a variable which controls which sense of execution is provided. To turn "guard checking on," by which we mean that guards are checked at runtime, execute the top-level form :set-guard-checking t. To turn it off, do :set-guard-checking nil. The status of this variable is reflected in the prompt. ACL2 !> means guard checking is on and ACL2 > means guard checking is off. The exclamation mark can be thought of as "barring" certain computations. The absence of the mark suggests the absence of error messages or unbarred access to the logical axioms. Thus, for example ACL2 !>(car 'abc) will signal an error, while ACL2 >(car 'abc) will return nil. Whether guards are checked during evaluation is independent of the default-defun-mode. We note this simply because it is easy to confuse ":program mode" with "evaluation in Common Lisp" and thus with "guard checking on;" and it is easy to confuse ":logic mode" with "evaluation in the logic" and with "guard checking off." But the default-defun-mode determines whether newly submitted definitions introduce programs or add logical axioms. That mode is independent of whether evaluation checks guards or not. You can operate in :logic mode with runtime guard checking on or off. Analogously, you can operate in :program mode with runtime guard checking on or off. However, one caveat is appropriate: functions introduced only as programs have no logical definitions and hence when they are evaluated their Common Lisp definitions must be used and thus their guards (if any) checked. That is, if you are defining functions in :program mode and evaluating expressions containing only such functions, guard checking may as well be on because guards are checked regardless. This same caveat applies to a few ACL2 system functions that take state as an argument. This list of functions includes all the keys of the alist *super-defun-wart-alist* and all function whose names are members of the list *initial-untouchables*. *Note GUARD:: for a general discussion of guards.  File: acl2-doc-lemacs.info, Node: SET-INHIBIT-OUTPUT-LST, Next: SKIP-PROOFS, Prev: SET-GUARD-CHECKING, Up: OTHER SET-INHIBIT-OUTPUT-LST control output Examples: (set-inhibit-output-lst '(warning)) (set-inhibit-output-lst '(proof-tree prove)) :set-inhibit-output-lst (proof-tree prove) General Form: (set-inhibit-output-lst lst) where lst is a form (which may mention state) that evaluates to a list of names, each of which is the name of one of the following "kinds" of output produced by ACL2. error error messages warning warnings observation observations prove commentary produced by the theorem prover event non-proof commentary produced by events such as defun and encapsulate summary the summary at the successful conclusion of an event proof-tree proof-tree output It is possible to inhibit each kind of output by putting the corresponding name into lst. For example, if 'warning is included in (the value of) lst, then no warnings are printed. Note that proof-tree output is affected by set-inhibit-output-lst; *Note PROOF-TREE::.  File: acl2-doc-lemacs.info, Node: SKIP-PROOFS, Next: THM, Prev: SET-INHIBIT-OUTPUT-LST, Up: OTHER SKIP-PROOFS skip proofs for an event -- a quick way to introduce unsoundness Example Form: (skip-proofs (defun foo (x) (if (atom x) nil (cons (car x) (foo (reverse (cdr x))))))) General Form: (skip-proofs event) where event is an event; *Note EVENTS::. Event is processed as usual except that the proof obligations usually generated are merely assumed. WARNING: Skip-proofs allows inconsistent events to be admitted to the logic. Use it at your own risk! Sometimes in the development of a formal model or proof it is convenient to skip the proofs required by a given event. By embedding the event in a skip-proofs form, you can avoid the proof burdens generated by the event, at the risk of introducing unsoundness. Below we list three illustrative situations in which you might find skip-proofs useful. 1. The termination argument for a proposed function definition is complicated. You presume you could admit it, but are not sure that your definition has the desired properties. By embedding the defun event in a skip-proofs you can "admit" the function and experiment with theorems about it before you pay the price of its admission. 2. You intend eventually to verify the guards for a definition but do not want to take the time now to pursue that. By embedding the verify-guards event in a skip-proofs you can get the system to behave as though the guards were verified. 3. You are repeatedly recertifying a book while making many experimental changes. A certain defthm in the book takes a very long time to prove and you believe the proof is not affected by the changes you are making. By embedding the defthm event in a skip-proofs you allow the theorem to be assumed without proof during the experimental recertifications. Unsoundness or Lisp errors may result if the presumptions underlying a use of skip-proofs are incorrect. Therefore, skip-proofs must be considered a dangerous (though useful) tool in system development. Roughly speaking, a defthm embedded in a skip-proofs is essentially a defaxiom, except that it is not noted as an axiom for the purposes of functional instantiation (*Note LEMMA-INSTANCE::). But a skipped defun is much more subtle since not only is the definitional equation being assumed but so are formulas relating to termination and type. The situation is also difficult to characterize if the skip-proofs events are within the scope of an encapsulate in which constrained functions are being introduced. In such contexts no clear logical story is maintained; in particular, constraints aren't properly tracked for definitions. A proof script involving skip-proofs should be regarded as work-in-progress, not as a completed proof with some unproved assumptions. A skip-proofs event represents a promise by the author to admit the given event without further axioms. ACL2 allows the certification of books containing skip-proofs events. This is contrary to the spirit of certified books, since one is supposedly assured by a valid certificate that a book has been "blessed." But certification, too, takes the view of skip-proofs as "work-in-progress" and so allows the author of the book to promise to finish. When such books are certified, a warning to the author is printed, reminding him or her of the incurred obligation. When books containing skip-proofs are included into a session, a warning to the user is printed, reminding the user that the book is in fact incomplete and possibly inconsistent.  File: acl2-doc-lemacs.info, Node: THM, Next: TRANS, Prev: SKIP-PROOFS, Up: OTHER THM prove a theorem Example: (thm (equal (app (app a b) c) (app a (app b c)))) Also *Note DEFTHM::. Unlike defthm, thm does not create an event; it merely causes the theorem prover to attempt a proof. General Form: (thm term :hints hints :otf-flg otf-flg :doc doc-string) where term is a term alleged to be a theorem, and hints, otf-flg and doc-string are as described in the corresponding :doc entries. The three keyword arguments above are all optional.  File: acl2-doc-lemacs.info, Node: TRANS, Next: TRANS1, Prev: THM, Up: OTHER TRANS print the macroexpansion of a form Examples: :trans (list a b c) :trans (caddr x) :trans (cond (p q) (r)) This function takes one argument, an alleged term, and translates it, expanding the macros in it completely. Either an error is caused or the formal meaning of the term is printed. We also print the "multiplicity" and "state-out" for the translated term. The multiplicity indicates how many values are returned (in the mv sense) and is always 1 or greater. State-out indicates whether and where a state is returned. If state-out is nil, the form does not return a state (either as its value or among its multiple values). If t, the form returns one value and it is a state. Otherwise, state-out is a number which indicates which of its multiple values is a state. For more, *Note TERM::.  File: acl2-doc-lemacs.info, Node: TRANS1, Prev: TRANS, Up: OTHER TRANS1 print the one-step macroexpansion of a form Examples: :trans1 (list a b c) :trans1 (caddr x) :trans1 (cond (p q) (r)) This function takes one argument, an alleged term, and expands the top-level macro in it for one step only. Either an error is caused, which happens when the form is not a call of a macro, or the result printed. Also *Note TRANS::, which translates the given form completely.  File: acl2-doc-lemacs.info, Node: PROGRAMMING, Next: PROOF-CHECKER, Prev: OTHER, Up: Top PROGRAMMING built-in ACL2 functions The built-in ACL2 functions that one typically uses in writing programs are listed below. See their individual documentations. We do not bother to document the some of the more obscure functions provided by ACL2 that do not correspond to functions of Common Lisp. * Menu: * *:: multiplication macro * *STANDARD-CI*:: an ACL2 character-based analogue of CLTL's *standard-input* * *STANDARD-CO*:: the ACL2 analogue of CLTL's *standard-output* * *STANDARD-OI*:: an ACL2 object-based analogue of CLTL's *standard-input* * +:: addition macro * -:: macro for subtraction and negation * /:: macro for division and reciprocal * /=:: test inequality of two numbers * 1+:: increment by 1 * 1-:: decrement by 1 * <:: less-than * <=:: less-than-or-equal test * =:: test equality (of two numbers, symbols, or characters) * >:: greater-than test * >=:: greater-than-or-equal test * ABS:: the absolute value of a rational number * ACL2-CHARACTERP:: recognizer for characters * ACL2-COMPLEX-RATIONALP:: recognizer for complex rationals * ACL2-NUMBERP:: recognizer for numbers * ACL2-USER:: a package the ACL2 user may prefer * ACONS:: constructor for association lists * ADD-TO-SET-EQ:: add a symbol to a list * ALISTP:: recognizer for association lists * ALPHA-CHAR-P:: recognizer for alphabetic characters * AND:: conjunction * APPEND:: concatenate two or more lists * ASH:: arithmetic shift operation * ASSOC:: look up key in association list, using eql as test * ASSOC-EQ:: look up key in association list, using eq as test * ASSOC-EQUAL:: look up key in association list * ASSOC-KEYWORD:: look up key in a keyword-value-listp * ASSOC-STRING-EQUAL:: look up key, a string, in association list * ATOM:: recognizer for atoms * ATOM-LISTP:: recognizer for a true list of atoms * BINARY-*:: multiplication function * BINARY-+:: addition function * BINARY-APPEND:: concatenate two lists * BOOLEANP:: recognizer for booleans * BUTLAST:: all but a final segment of a list * CAAAAR:: car of the caaar * CAAADR:: car of the caadr * CAAAR:: car of the caar * CAADAR:: car of the cadar * CAADDR:: car of the caddr * CAADR:: car of the cadr * CAAR:: car of the car * CADAAR:: car of the cdaar * CADADR:: car of the cdadr * CADAR:: car of the cdar * CADDAR:: car of the cddar * CADDDR:: car of the cdddr * CADDR:: car of the cddr * CADR:: car of the cdr * CAR:: returns the first element of a non-empty list, else nil * CASE:: conditional based on if-then-else using eql * CASE-MATCH:: pattern matching or destructuring * CDAAAR:: cdr of the caaar * CDAADR:: cdr of the caadr * CDAAR:: cdr of the caar * CDADAR:: cdr of the cadar * CDADDR:: cdr of the caddr * CDADR:: cdr of the cadr * CDAR:: cdr of the car * CDDAAR:: cdr of the cdaar * CDDADR:: cdr of the cdadr * CDDAR:: cdr of the cdar * CDDDAR:: cdr of the cddar * CDDDDR:: cdr of the cdddr * CDDDR:: cdr of the cddr * CDDR:: cdr of the cdr * CDR:: returns the second element of a cons pair, else nil * CEILING:: division returning an integer by truncating toward positive infinity * CHAR:: the nth element (zero-based) of a string * CHAR-CODE:: the numeric code for a given character * CHAR-DOWNCASE:: turn upper-case characters into lower-case characters * CHAR-EQUAL:: character equality without regard to case * CHAR-UPCASE:: turn lower-case characters into upper-case characters * CHAR<:: less-than test for characters * CHAR<=:: less-than-or-equal test for characters * CHAR>:: greater-than test for characters * CHAR>=:: greater-than-or-equal test for characters * CHARACTER-LISTP:: recognizer for a true list of characters * CHARACTERS:: characters in ACL2 * CODE-CHAR:: the character corresponding to a given numeric code * COERCE:: coerce a character list to a string and a string to a list * COMPILATION:: compiling ACL2 functions * COMPLEX:: create an ACL2 number * COMPLEX-RATIONALP:: recognizes complex rational numbers * CONCATENATE:: concatenate lists or strings together * COND:: conditional based on if-then-else * CONJUGATE:: complex number conjugate * CONS:: pair and list constructor * CONSP:: recognizer for cons pairs * DECLARE:: declarations * DENOMINATOR:: divisor of a ratio in lowest terms * DIGIT-CHAR-P:: the number, if any, corresponding to a given character * DIGIT-TO-CHAR:: map a digit to a character * EIGHTH:: eighth member of the list * ENDP:: recognizer for empty lists * EQ:: equality of symbols * EQL:: test equality (of two numbers, symbols, or characters) * EQLABLE-ALISTP:: recognizer for a true list of pairs whose cars are suitable for eql * EQLABLE-LISTP:: recognizer for a true list of objects each suitable for eql * EQLABLEP:: the guard for the function eql * EQUAL:: true equality * ER-PROGN:: perform a sequence of state-changing "error triples" * EVENP:: test whether an integer is even * EXPLODE-NONNEGATIVE-INTEGER:: the list of characters in the decimal form of a number * EXPT:: exponential function * FIFTH:: fifth member of the list * FIRST:: first member of the list * FIX:: coerce to a number * FIX-TRUE-LIST:: coerce to a true list * FLOOR:: division returning an integer by truncating toward negative infinity * FMS:: :(str alist co-channel state evisc) => state * FMT:: formatted printing * FMT1:: :(str alist col co-channel state evisc) => (mv col state) * FOURTH:: fourth member of the list * IDENTITY:: the identity function * IF:: if-then-else function * IFF:: logical "if and only if" * IFIX:: coerce to an integer * ILLEGAL:: cause a hard error * IMAGPART:: imaginary part of a complex number * IMPLIES:: logical implication * IMPROPER-CONSP:: recognizer for improper (non-null-terminated) non-empty lists * INT=:: test equality of two integers * INTEGER-LENGTH:: number of bits in two's complement integer representation * INTEGER-LISTP:: recognizer for a true list of integers * INTEGERP:: recognizer for whole numbers * INTERN:: create a new symbol in a given package * INTERN-IN-PACKAGE-OF-SYMBOL:: create a symbol with a given name * INTERSECTP-EQ:: test whether two lists of symbols intersect * INTERSECTP-EQUAL:: test whether two lists intersect * IO:: input/output facilities in ACL2 * IRRELEVANT-FORMALS:: formals that are used but only insignificantly * KEYWORD-VALUE-LISTP:: recognizer for true lists whose even-position elements are keywords * KEYWORDP:: recognizer for keywords * LAST:: the last cons (not element) of a list * LENGTH:: length of a string or proper list * LET:: binding of lexically scoped (local) variables * LET*:: binding of lexically scoped (local) variables * LIST:: build a list * LIST*:: build a list * LISTP:: recognizer for (not necessarily proper) lists * LOGAND:: bitwise logical `and' of two integers * LOGANDC1:: bitwise logical `and' of two ints, complementing the first * LOGANDC2:: bitwise logical `and' of two ints, complementing the second * LOGBITP:: the ith bit of an integer * LOGCOUNT:: number of "on" bits in a two's complement number * LOGEQV:: bitwise logical equivalence of two integers * LOGIOR:: bitwise logical inclusive or of two integers * LOGNAND:: bitwise logical `nand' of two integers * LOGNOR:: bitwise logical `nor' of two integers * LOGNOT:: bitwise not of a two's complement number * LOGORC1:: bitwise logical inclusive or of two ints, complementing the first * LOGORC2:: bitwise logical inclusive or of two ints, complementing the second * LOGTEST:: test if two integers share a `1' bit * LOGXOR:: bitwise logical exclusive or of two integers * LOWER-CASE-P:: recognizer for lower case characters * MAKE-CHARACTER-LIST:: coerce to a list of characters * MAKE-LIST:: make a list of a given size * MAX:: the larger of two rational numbers * MEMBER:: membership predicate, using eql as test * MEMBER-EQ:: membership predicate, using eq as test * MEMBER-EQUAL:: membership predicate * MIN:: the smaller of two rational numbers * MINUSP:: test whether a rational number is negative * MOD:: remainder using floor * MV:: returning multiple values * MV-LET:: calling multi-valued ACL2 functions * MV-NTH:: the mv-nth element (zero-based) of a list * NFIX:: coerce to a natural number * NINTH:: ninth member of the list * NO-DUPLICATESP:: check for duplicates in a list * NONNEGATIVE-INTEGER-QUOTIENT:: natural number division function * NOT:: logical negation * NTH:: the nth element (zero-based) of a list * NTHCDR:: final segment of a list * NULL:: recognizer for the empty list * NUMERATOR:: dividend of a ratio in lowest terms * ODDP:: test whether an integer is odd * OR:: conjunction * PAIRLIS:: see pairlis$ * PAIRLIS$:: zipper together two lists * PLUSP:: test whether a rational number is positive * POSITION:: position of an item in a string or a list, using eql as test * POSITION-EQ:: position of an item in a string or a list, using eq as test * POSITION-EQUAL:: position of an item in a string or a list * PPROGN:: evaluate a sequence of forms that return state * PROGN:: see the documentation for er-progn * PROOFS-CO:: the proofs character output channel * PROPER-CONSP:: recognizer for proper (null-terminated) non-empty lists * PUT-ASSOC-EQ:: modify an association list by associating a value with a key * PUT-ASSOC-EQUAL:: modify an association list by associating a value with a key * RASSOC:: look up value in association list, using eql as test * RATIONAL-LISTP:: recognizer for a true list of rational numbers * RATIONALP:: recognizer for whole numbers * REALPART:: real part of a complex number * REDEFINING-PROGRAMS:: an explanation of why we restrict redefinitions * REM:: remainder using truncate * REMOVE:: remove all occurrences, testing using eql * REMOVE-DUPLICATES:: remove duplicates from a string or (using eql) a list * REMOVE-DUPLICATES-EQUAL:: remove duplicates from a list * REST:: rest (cdr) of the list * REVAPPEND:: concatentate the reverse of one list to another * REVERSE:: reverse a list * RFIX:: coerce to a rational number * ROUND:: division returning an integer by rounding off * SECOND:: second member of the list * SET-DIFFERENCE-EQUAL:: elements of one list that are not elements of another * SEVENTH:: seventh member of the list * SIGNUM:: indicator for positive, negative, or zero * SIXTH:: sixth member of the list * STANDARD-CHAR-LISTP:: recognizer for standard characters * STANDARD-CHAR-P:: recognizer for standard characters * STANDARD-CO:: the character output channel to which ld prints * STANDARD-OI:: the standard object input "channel" * STRING:: coerce to a string * STRING-ALISTP:: recognizer for association lists with strings as keys * STRING-APPEND:: concatenate two strings * STRING-DOWNCASE:: in a given string, turn upper-case characters into lower-case * STRING-EQUAL:: string equality without regard to case * STRING-LISTP:: recognizer for a true list of strings * STRING-UPCASE:: in a given string, turn lower-case characters into upper-case * STRING<:: less-than test for strings * STRING<=:: less-than-or-equal test for strings * STRING>:: greater-than test for strings * STRING>=:: less-than-or-equal test for strings * STRINGP:: recognizer for strings * STRIP-CARS:: collect up all first components of pairs in a list * STRIP-CDRS:: collect up all second components of pairs in a list * SUBLIS:: substitute an alist into a tree * SUBSEQ:: subsequence of a string or list * SUBSETP:: test if every member of one list is a member of the other * SUBSETP-EQUAL:: check if all members of one list are members of the other * SUBST:: a single substitution into a tree * SYMBOL-<:: less-than test for symbols * SYMBOL-ALISTP:: recognizer for association lists with symbols as keys * SYMBOL-LISTP:: recognizer for a true list of symbols * SYMBOL-NAME:: the name of a symbol (a string) * SYMBOL-PACKAGE-NAME:: the name of the package of a symbol (a string) * SYMBOLP:: recognizer for symbols * TAKE:: initial segment of a list * TENTH:: tenth member of the list * THE:: run-time type check * THIRD:: third member of the list * TRUE-LIST-LISTP:: recognizer for true (proper) lists of true lists * TRUE-LISTP:: recognizer for proper (null-terminated) lists * TRUNCATE:: division returning an integer by truncating toward 0 * TYPE-SPEC:: type specifiers in declarations * UNARY--:: arithmetic negation function * UNARY-/:: reciprocal function * UNION-EQ:: union of two lists of symbols * UNION-EQUAL:: union of two lists * UPDATE-NTH:: modify a list by putting the given value at the given position * UPPER-CASE-P:: recognizer for upper case characters * ZERO-TEST-IDIOMS:: how to test for 0 * ZEROP:: test an acl2-number against 0 * ZIP:: testing an "integer" against 0 * ZP:: testing a "natural" against 0 Related topics other than immediate subtopics: * ACL2-CUSTOMIZATION:: customizing ACL2 for a particular user * ARRAYS:: an introduction to ACL2 arrays. * CERTIFY-BOOK:: how to produce a certificate for a book * COMP:: compile some ACL2 functions * DEFCONST:: define a constant * DEFPKG:: define a new symbol package * DEFUN:: define a function symbol * INCLUDE-BOOK:: load the events in a file * MUTUAL-RECURSION:: define some mutually recursive functions * SET-COMPILE-FNS:: have each function compiled as you go along. * SET-IGNORE-OK:: allow unused formals and locals without an ignore declaration * SET-IRRELEVANT-FORMALS-OK:: allow irrelevant formals in definitions See any documentation for Common Lisp for more details on many of these functions.  File: acl2-doc-lemacs.info, Node: *, Next: *STANDARD-CI*, Prev: PROGRAMMING, Up: PROGRAMMING * multiplication macro * 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))). *Note BINARY-*::. * is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: *STANDARD-CI*, Next: *STANDARD-CO*, Prev: *, Up: PROGRAMMING *STANDARD-CI* an ACL2 character-based analogue of CLTL's *standard-input* 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*. *Note *STANDARD-CO*::.  File: acl2-doc-lemacs.info, Node: *STANDARD-CO*, Next: *STANDARD-OI*, Prev: *STANDARD-CI*, Up: PROGRAMMING *STANDARD-CO* the ACL2 analogue of CLTL's *standard-output* 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. *Note STANDARD-OI:: and *Note STANDARD-CO::.  File: acl2-doc-lemacs.info, Node: *STANDARD-OI*, Next: +, Prev: *STANDARD-CO*, Up: PROGRAMMING *STANDARD-OI* an ACL2 object-based analogue of CLTL's *standard-input* 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*. *Note *STANDARD-CO*::.  File: acl2-doc-lemacs.info, Node: +, Next: -, Prev: *STANDARD-OI*, Up: PROGRAMMING + addition macro + 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))). *Note BINARY-+::.  File: acl2-doc-lemacs.info, Node: -, Next: /, Prev: +, Up: PROGRAMMING - macro for subtraction and negation *Note BINARY-+:: for addition and *Note 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).  File: acl2-doc-lemacs.info, Node: /, Next: /=, Prev: -, Up: PROGRAMMING / macro for division and reciprocal *Note BINARY-*:: for multiplication and *Note 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.  File: acl2-doc-lemacs.info, Node: /=, Next: 1+, Prev: /, Up: PROGRAMMING /= test inequality of two numbers (/= 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, *Note ZERO-TEST-IDIOMS::. /= is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: 1+, Next: 1-, Prev: /=, Up: PROGRAMMING 1+ increment by 1 (1+ x) is the same as (+ 1 x). *Note +::. 1+ is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: 1-, Next: <, Prev: 1+, Up: PROGRAMMING 1- decrement by 1 (1- x) is the same as (- x 1). *Note -::. 1- is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: <, Next: <=, Prev: 1-, Up: PROGRAMMING < less-than Basic 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.  File: acl2-doc-lemacs.info, Node: <=, Next: =, Prev: <, Up: PROGRAMMING <= less-than-or-equal test <= is a macro, and (<= x y) expands to the same thing as (not (< y x)). *Note <::. <= is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: =, Next: >, Prev: <=, Up: PROGRAMMING = test equality (of two numbers, symbols, or characters) (= 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, *Note ZERO-TEST-IDIOMS::. = is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: >, Next: >=, Prev: =, Up: PROGRAMMING > greater-than test > is a macro, and (> x y) expands to the same thing as (< y x). *Note <::. > is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: >=, Next: ABS, Prev: >, Up: PROGRAMMING >= greater-than-or-equal test >= is a macro, and (>= x y) expands to the same thing as (not (< x y)). *Note <::. >= is a Common Lisp function. See any Common Lisp documentation for more information.  File: acl2-doc-lemacs.info, Node: ABS, Next: ACL2-CHARACTERP, Prev: >=, Up: PROGRAMMING ABS the absolute value of a rational number (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 (*Note COMPLEX-RATIONALP::) and hence not an ACL2 object.  File: acl2-doc-lemacs.info, Node: ACL2-CHARACTERP, Next: ACL2-COMPLEX-RATIONALP, Prev: ABS, Up: PROGRAMMING ACL2-CHARACTERP recognizer for characters (acl2-characterp x) is true if and only if x is a character.  File: acl2-doc-lemacs.info, Node: ACL2-COMPLEX-RATIONALP, Next: ACL2-NUMBERP, Prev: ACL2-CHARACTERP, Up: PROGRAMMING ACL2-COMPLEX-RATIONALP recognizer for complex rationals (acl2-complex-rationalp x) is true if and only if x is a complex rational number (and hence, not a rational number).  File: acl2-doc-lemacs.info, Node: ACL2-NUMBERP, Next: ACL2-USER, Prev: ACL2-COMPLEX-RATIONALP, Up: PROGRAMMING ACL2-NUMBERP recognizer for numbers (acl2-numberp x) is true if and only if x is a number, i.e., a rational or complex rational number.  File: acl2-doc-lemacs.info, Node: ACL2-USER, Next: ACONS, Prev: ACL2-NUMBERP, Up: PROGRAMMING ACL2-USER a package the ACL2 user may prefer 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 (*Note 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".  File: acl2-doc-lemacs.info, Node: ACONS, Next: ADD-TO-SET-EQ, Prev: ACL2-USER, Up: PROGRAMMING ACONS constructor for association lists (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.  File: acl2-doc-lemacs.info, Node: ADD-TO-SET-EQ, Next: ALISTP, Prev: ACONS, Up: PROGRAMMING ADD-TO-SET-EQ add a symbol to a list 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 x. (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.  File: acl2-doc-lemacs.info, Node: ALISTP, Next: ALPHA-CHAR-P, Prev: ADD-TO-SET-EQ, Up: PROGRAMMING ALISTP recognizer for association lists (alistp x) is true if and only if x is a list of cons pairs. (alistp x) has a guard of t.  File: acl2-doc-lemacs.info, Node: ALPHA-CHAR-P, Next: AND, Prev: ALISTP, Up: PROGRAMMING ALPHA-CHAR-P recognizer for alphabetic characters (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.  File: acl2-doc-lemacs.info, Node: AND, Next: APPEND, Prev: ALPHA-CHAR-P, Up: PROGRAMMING AND conjunction 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.  File: acl2-doc-lemacs.info, Node: APPEND, Next: ASH, Prev: AND, Up: PROGRAMMING APPEND concatenate two or more lists 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.  File: acl2-doc-lemacs.info, Node: ASH, Next: ASSOC, Prev: APPEND, Up: PROGRAMMING ASH arithmetic shift operation (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.  File: acl2-doc-lemacs.info, Node: ASSOC, Next: ASSOC-EQ, Prev: ASH, Up: PROGRAMMING ASSOC look up key in association list, using eql as test (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. *Note ASSOC-EQUAL:: and *Note 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.  File: acl2-doc-lemacs.info, Node: ASSOC-EQ, Next: ASSOC-EQUAL, Prev: ASSOC, Up: PROGRAMMING ASSOC-EQ look up key in association list, using eq as test (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 (*Note ALISTP::), and moreover, either x is a symbol or all keys of alist are symbols, i.e., alist is a symbol-alistp.  File: acl2-doc-lemacs.info, Node: ASSOC-EQUAL, Next: ASSOC-KEYWORD, Prev: ASSOC-EQ, Up: PROGRAMMING ASSOC-EQUAL look up key in association list (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. *Note ASSOC:: and *Note ASSOC-EQ::.  File: acl2-doc-lemacs.info, Node: ASSOC-KEYWORD, Next: ASSOC-STRING-EQUAL, Prev: ASSOC-EQUAL, Up: PROGRAMMING ASSOC-KEYWORD look up key in a keyword-value-listp 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).  File: acl2-doc-lemacs.info, Node: ASSOC-STRING-EQUAL, Next: ATOM, Prev: ASSOC-KEYWORD, Up: PROGRAMMING ASSOC-STRING-EQUAL look up key, a string, in association list (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.  File: acl2-doc-lemacs.info, Node: ATOM, Next: ATOM-LISTP, Prev: ASSOC-STRING-EQUAL, Up: PROGRAMMING ATOM recognizer for atoms (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.  File: acl2-doc-lemacs.info, Node: ATOM-LISTP, Next: BINARY-*, Prev: ATOM, Up: PROGRAMMING ATOM-LISTP recognizer for a true list of atoms The predicate atom-listp tests whether its argument is a true-listp of atoms, i.e., of non-conses.  File: acl2-doc-lemacs.info, Node: BINARY-*, Next: BINARY-+, Prev: ATOM-LISTP, Up: PROGRAMMING BINARY-* multiplication function Basic 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-*; *Note *::.  File: acl2-doc-lemacs.info, Node: BINARY-+, Next: BINARY-APPEND, Prev: BINARY-*, Up: PROGRAMMING BINARY-+ addition function Basic 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-+; *Note +::.  File: acl2-doc-lemacs.info, Node: BINARY-APPEND, Next: BOOLEANP, Prev: BINARY-+, Up: PROGRAMMING BINARY-APPEND concatenate two lists This binary function implements append, which is a macro in ACL2. *Note APPEND:: The guard for binary-append requires the first argument to be a true-listp.  File: acl2-doc-lemacs.info, Node: BOOLEANP, Next: BUTLAST, Prev: BINARY-APPEND, Up: PROGRAMMING BOOLEANP recognizer for booleans (Booleanp x) is t if x is t or nil, and is nil otherwise. *Note 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?  File: acl2-doc-lemacs.info, Node: BUTLAST, Next: CAAAAR, Prev: BOOLEANP, Up: PROGRAMMING BUTLAST all but a final segment of a list (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, *Note TAKE:: and *Note 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.  File: acl2-doc-lemacs.info, Node: CAAAAR, Next: CAAADR, Prev: BUTLAST, Up: PROGRAMMING CAAAAR car of the caaar See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CAAADR, Next: CAAAR, Prev: CAAAAR, Up: PROGRAMMING CAAADR car of the caadr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CAAAR, Next: CAADAR, Prev: CAAADR, Up: PROGRAMMING CAAAR car of the caar See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CAADAR, Next: CAADDR, Prev: CAAAR, Up: PROGRAMMING CAADAR car of the cadar See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CAADDR, Next: CAADR, Prev: CAADAR, Up: PROGRAMMING CAADDR car of the caddr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CAADR, Next: CAAR, Prev: CAADDR, Up: PROGRAMMING CAADR car of the cadr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CAAR, Next: CADAAR, Prev: CAADR, Up: PROGRAMMING CAAR car of the car See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CADAAR, Next: CADADR, Prev: CAAR, Up: PROGRAMMING CADAAR car of the cdaar See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CADADR, Next: CADAR, Prev: CADAAR, Up: PROGRAMMING CADADR car of the cdadr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CADAR, Next: CADDAR, Prev: CADADR, Up: PROGRAMMING CADAR car of the cdar See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CADDAR, Next: CADDDR, Prev: CADAR, Up: PROGRAMMING CADDAR car of the cddar See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CADDDR, Next: CADDR, Prev: CADDAR, Up: PROGRAMMING CADDDR car of the cdddr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CADDR, Next: CADR, Prev: CADDDR, Up: PROGRAMMING CADDR car of the cddr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CADR, Next: CAR, Prev: CADDR, Up: PROGRAMMING CADR car of the cdr See any Common Lisp documentation for details.  File: acl2-doc-lemacs.info, Node: CAR, Next: CASE, Prev: CADR, Up: PROGRAMMING CAR returns the first element of a non-empty list, else nil Basic 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.