a name created by a logical event
Parent topic: MISCELLANEOUS Home
Examples: assoc caddr + "ACL2-USER" "arith" "project/task-1/arith.lisp" :here
A logical name is either a name introduced by some event, such as
defun, defthm, or include-book, or else is the keyword :here, which
refers to the most recent such event. See events. Every
logical name is either a symbol or a string. For the syntactic
rules on names, see name. The symbols name functions, macros,
constants, axioms, theorems, labels, and theories. The strings name
packages or books. We permit the keyword symbol :here to be used as
a logical name denoting the most recently completed event.
The logical name introduced by an include-book is the full book name
string for the book (see full-book-name). Thus, under the
appropriate setting for the current book directory (see cbd)
the event (include-book "arith") may introduce the logical name
"/usr/home/smith/project/task-1/arith.lisp" .Under a different
cbd setting, it may introduce a different
logical name, perhaps
"/local/src/acl2/library/arith.lisp" .It is possible that identical
include-book events forms in a
session introduce two different logical names because of the current
book directory.
A logical name that is a string is either a package name or a book
name. If it is not a package name, we support various conventions
to interpret it as a book name. If it does not end with the string
".lisp" we extend it appropriately. Then, we search for any book
name that has the given logical name as a terminal substring.
Suppose (include-book "arith") is the only include-book so far and
that "/usr/home/smith/project/task-1/arith.lisp" is the source
file it processed. Then "arith", "arith.lisp" and
"task-1/arith.lisp" are all logical names identifying that
include-book event (unless they are package names). Now suppose a
second (include-book "arith") is executed and processes
"/local/src/acl2/library/arith.lisp". Then "arith" is no longer
a logical name, because it is ambiguous. However, "task-1/arith"
is a logical name for the first include-book and "library/arith"
is a logical name for the second. Indeed, the first can be named by
"1/arith" and the second by "y/arith".
Logical names are used primarily in the theory manipulation
functions, e.g., universal-theory and current-theory with which you
may obtain some standard theories as of some point in the historical
past. The reference points are the introductions of logical names,
i.e., the past is determined by the events it contains. One might
ask, ``Why not discuss the past with the much more flexible language
of command descriptors?'' (See command-descriptor.) The reason
is that inside of such events as encapsulate or macro commands that
expand to progns of events, command descriptors provide too coarse a
grain.
When logical names are used as referents in theory expressions used in books, one must consider the possibility that the defining event within the book in question becomes redundant by the definition of the name prior to the assumption of the book. See redundant-events.
limit application of permutative rewrite rules
Parent topic: MISCELLANEOUS Home
See rule-classes for a discussion of the syntax of the
:loop-stopper field of :rewrite rule-classes. Here we describe how
that field is used, and also how that field is created when the user
does not explicitly supply it.
For example, the built-in :rewrite rule commutativity-of-+,
(implies (and (acl2-numberp x)
(acl2-numberp y))
(equal (+ x y) (+ y x))),
creates a rewrite rule with a loop-stopper of ((x y binary-+)).
This means, very roughly, that the term corresponding to y must be
``smaller'' than the term corresponding to x in order for this rule
to apply. However, the presence of binary-+ in the list means that
certain functions that are ``invisible'' with respect to binary-+
(by default, unary-- is the only such function) are more or less
ignored when making this ``smaller'' test. We are much more precise
below.
Our explanation of loop-stopping is in four parts. First we discuss
ACL2's notion of ``term order.'' Next, we bring in the notion of
``invisibility'', and use it together with term order to define
orderings on terms that are used in the loop-stopping algorithm.
Third, we describe that algorithm. These topics all assume that we
have in hand the :loop-stopper field of a given rewrite rule; the
fourth and final topic describes how that field is calculated when
it is not supplied by the user.
ACL2 must sometimes decide which of two terms is syntactically
simpler. It uses a total ordering on terms, called the ``term
order.'' Under this ordering constants such as '(a b c) are simpler
than terms containing variables such as x and (+ 1 x). Terms
containing variables are ordered according to how many occurrences
of variables there are. Thus x and (+ 1 x) are both simpler than
(cons x x) and (+ x y). If variable counts do not decide the order,
then the number of function applications are tried. Thus (cons x x)
is simpler than (+ x (+ 1 y)) because the latter has one more
function application. Finally, if the number of function
applications do not decide the order, a lexicographic ordering on
Lisp objects is used. See term-order for details.
When the loop-stopping algorithm is controlling the use of
permutative :rewrite rules it allows term1 to be moved leftward over
term2 only if term1 is smaller, in a suitable sense. Note: The
sense used in loop-stopping is not the above explained term order
but a more complicated ordering described below. The use of a total
ordering stops rules like commutativity from looping indefinitely
because it allows (+ b a) to be permuted to (+ a b) but not vice
versa, assuming a is smaller than b in the ordering. Given a set of
permutative rules that allows arbitrary permutations of the tips of
a tree of function calls, this will normalize the tree so that the
smallest argument is leftmost and the arguments ascend in the order
toward the right. Thus, for example, if the same argument appears
twice in the tree, as x does in the binary-+ tree denoted by the
term (+ a x b x), then when the allowed permutations are done, all
occurrences of the duplicated argument in the tree will be adjacent,
e.g., the tree above will be normalized to (+ a b x x).
Suppose the loop-stopping algorithm used term order, as noted above,
and consider the binary-+ tree denoted by (+ x y (- x)). The
arguments here are in ascending term order already. Thus, no
permutative rules are applied. But because we are inside a
+-expression it is very convenient if x and (- x) could be given
virtually the same position in the ordering so that y is not
allowed to separate them. This would allow such rules as
(+ i (- i) j) = j to be applied. In support of this, the
ordering used in the control of permutative rules allows certain
unary functions, e.g., the unary minus function above, to be
``invisible'' with respect to certain ``surrounding'' functions,
e.g., + function above.
Briefly, a unary function symbol fn1 is invisible with respect to a
function symbol fn2 if fn2 belongs to the value of fn1 in
invisible-fns-alist; also see set-invisible-fns-alist, which
explains its format and how it can be set by the user. Roughly
speaking, ``invisible'' function symbols are ignored for the
purposes of the term-order test.
Consider the example above, (+ x y (- x)). The translated version
of this term is (binary-+ x (binary-+ y (unary-- x))). The initial
invisible-fns-alist makes unary-- invisible with repect to binary-+.
The commutativity rule for binary-+ will attempt to swap y and
(unary-- x) and the loop-stopping algorithm is called to approve or
disapprove. If term order is used, the swap will be disapproved.
But term order is not used. While the loop-stopping algorithm is
permuting arguments inside a binary-+ expression, unary-- is
invisible. Thus, insted of comparing y with (unary-- x), the
loop-stopping algorithm compares y with x, approving the swap
because x comes before y.
Here is a more precise specification of the total order used for
loop-stopping with respect to a list, fns, of functions that are to
be considered invisible. Let x and y be distinct terms; we specify
when ``x is smaller than y with respect to fns.'' If x is the
application of a unary function symbol that belongs to fns, replace
x by its argument. Repeat this process until the result is not the
application of such a function; let us call the result x-guts.
Similarly obtain y-guts from y. Now if x-guts is the same term as
y-guts, then x is smaller than y in this order iff x is smaller than
y in the standard term order. On the other hand, if x-guts is
different than y-guts, then x is smaller than y in this order iff
x-guts is smaller than y-guts in the standard term order.
Now we may describe the loop-stopping algorithm. Consider a rewrite
rule with conclusion (equiv lhs rhs) that applies to a term x in a
given context; see rewrite. Suppose that this rewrite rule has
a loop-stopper field (technically, the :heuristic-info field) of
((x1 y1 . fns-1) ... (xn yn . fns-n)). (Note that this field can be
observed by using the command :pr with the name of the rule;
see pr.) We describe when rewriting is permitted. The
simplest case is when the loop-stopper list is nil (i.e., n is 0);
in that case, rewriting is permitted. Otherwise, for each i from 1
to n let xi' be the actual term corresponding to the variable xi
when lhs is matched against the term to be rewritten, and similarly
correspond yi' with y. If xi' and yi' are the same term for all i,
then rewriting is not permitted. Otherwise, let k be the least i
such that xi' and yi' are distinct. Let fns be the list of all
functions that are invisible with respect to every function in
fns-k, if fns-k is non-empty; otherwise, let fns be nil. Then
rewriting is permitted if and only if yi' is smaller than xi' with
respect to fns, in the sense defined in the preceding paragraph.
It remains only to describe how the loop-stopper field is calculated
for a rewrite rule when this field is not supplied by the user. (On
the other hand, to see how the user may specify the :loop-stopper,
see rule-classes.) Suppose the conclusion of the rule is of
the form (equiv lhs rhs). First of all, if rhs is not an instance
of the left hand side by a substitution whose range is a list of
distinct variables, then the loop-stopper field is nil. Otherwise,
consider all pairs (u . v) from this substitution with the property
that the first occurrence of v appears in front of the first
occurrence of u in the print representation of rhs. For each such u
and v, form a list fns of all functions fn in lhs with the property
that u or v (or both) appears as a top-level argument of a subterm
of lhs with function symbol fn. Then the loop-stopper for this
rewrite rule is a list of all lists (u v . fns).
the Common Lisp entry to ACL2
Parent topic: MISCELLANEOUS Home
To enter the ACL2 command loop from Common Lisp, call the Common
Lisp program lp (which stands for ``loop,'' as in ``read-eval-print
loop'' or ``command loop.'') The ACL2 command loop is actually
coded in ACL2 as the function ld (which stands for ``load''). The
command loop is just what you get by loading from the standard
object input channel, *standard-oi*. Calling ld directly from
Common Lisp is possible but fragile because hard lisp errors or
aborts throw you out of ld and back to the top-level of Common Lisp.
Lp calls ld in such a way as to prevent this and is thus the
standard way to get into the ACL2 command loop. Also
see acl2-customization for information on the loading of an
initialization file.
All of the visible functionality of lp is in fact provided by ld,
which is written in ACL2 itself. Therefore, you should see ld
for detailed documentation of the ACL2 command loop. We sketch it
below, for novice users.
Every expression typed to the ACL2 top-level must be an ACL2 expression.
Any ACL2 expression containing no variables may be evaluated.
Because of the applicative nature of ACL2, we make a special
exception for the variable state. If this variable occurs in the
form, it is taken to mean the ``current'' ACL2 state object. If the
form returns a new state object as one of its values, then that is
considered the new ``current'' state for the evaluation of the
subsequent form. See state.
If the form read is a single keyword, e.g., :pe or :ubt, then
special procedures are followed. See keyword-commands.
The command loop keeps track of the commands you have typed and allows you to review them, display them, and roll the logical state back to that created by any command. See history.
ACL2 makes the convention that if a top-level form returns three
values, the last of which is an ACL2 state, then the first is
treated as a flag that means ``an error occurred,'' the second is
the value to be printed if no error occurred, and the third is (of
course) the new state. When ``an error occurs'' no value is
printed. Thus, if you execute a top-level form that happens to
return three such values, only the second will be printed (and that
will only happen if the first is nil!). See ld for details.
the formals list of a macro definition
Parent topic: MISCELLANEOUS Home
Examples: (x y z) (x y z &optional max (base '10 basep)) (x y &rest rst) (x y &key max base) (&whole sexpr x y)
The ``lambda-list'' of a macro definition may include simple formal
parameter names as well as appropriate uses of the following
lambda-list keywords from CLTL (pp. 60 and 145):
&optional, &rest, &key, &whole, &body, and &allow-other-keys.ACL2 does not support
&aux and &environment. In addition, we make
the following restrictions:
You are encouraged to experiment with the macro facility. One way to do so is to define a macro that does nothing but return the quotation of its arguments, e.g.,(1) initialization forms in
&optionaland&keyspecifiers must be quoted values;(2)
&allow-other-keysmay only be used once, as the last specifier; and(3) destructuring is not allowed.
(defmacro demo (x y &optional opt &key key1 key2) (list 'quote (list x y opt key1 key2)))You may then execute the macro on some sample forms, e.g.,
term value
(demo 1 2) (1 2 NIL NIL NIL)
(demo 1 2 3) (1 2 3 NIL NIL)
(demo 1 2 :key1 3) error: non-even key/value arglist
(because :key1 is used as opt)
(demo 1 2 3 :key2 5) (1 2 3 NIL 5)
Also see trans.
syntactic rules on logical names
Parent topic: MISCELLANEOUS Home
Examples Counter-ExamplesPRIMEP 91 (not a symbolp) F-AC-23 :CHK-LIST (in KEYWORD package) 1AX *PACKAGE* (in the Lisp Package) |Prime Number| 1E3 (not a symbolp)
Many different ACL2 entities have names, e.g., functions, macros,
variables, constants, packages, theorems, theories, etc.
Package names are strings. All other names are symbols and may not
be in the "KEYWORD" package. Moreover, names of functions,
macros, constrained functions, and constants, other than those that
are predefined, must not be in the ``main Lisp package'' (which is
("LISP" or "COMMON-LISP", according to whether we are
following CLTL1 or CLTL2). An analogous restriction on variables
is given below.
T, nil, and all names above except those that begin with ampersand
(&) are names of variables or constants. T, nil, and those names
beginning and ending with star (*) are constants. All other such
names are variables.
Note that names that start with ampersand, such as &rest, may be
lambda list keywords and are reserved for such use whether or not
they are in the CLTL constant lambda-list-keywords. (See pg 82
of CLTL2.) That is, these may not be used as variables. Unlike
constants, variables may be in the main Lisp package as long as they
are in the original list of imports from that package to ACL2, the
list *common-lisp-symbols-from-main-lisp-package*, and do not
belong to a list of symbols that are potentially ``global.'' This
latter list is the value of *common-lisp-specials-and-constants*.
Our restrictions pertaining to the main Lisp package take into
account that some symbols, e.g., lambda-list-keywords and
boole-c2, are ``special.'' Permitting them to be bound could
have harmful effects. In addition, the Common Lisp language does
not allow certain manipulations with many symbols of that package.
So, we stay away from them, except for allowing certain variables as
indicated above.
ordered binary decision diagrams with rewriting
Parent topic: MISCELLANEOUS Home
See bdd for information on this topic.
pushing all the initial subgoals
Parent topic: MISCELLANEOUS Home
The value of this flag is normally nil. If you want to prevent the
theorem prover from abandoning its initial work upon pushing the
second subgoal, set :otf-flg to t.
Suppose you submit a conjecture to the theorem prover and the system
splits it up into many subgoals. Any subgoal not proved by other
methods is eventually set aside for an attempted induction proof.
But upon setting aside the second such subgoal, the system chickens
out and decides that rather than prove n>1 subgoals inductively, it
will abandon its initial work and attempt induction on the
originally submitted conjecture. The :otf-flg (Onward Thru the Fog)
allows you to override this chickening out. When :otf-flg is t, the
system will push all the initial subgoals and proceed to try to
prove each, independently, by induction.
Even when you don't expect induction to be used or to succeed,
setting the :otf-flg is a good way to force the system to generate
and display all the initial subgoals.
re-defining undone defpkgs
Parent topic: MISCELLANEOUS Home
Suppose (defpkg "pkg" imports) is the most recently executed
successful definition of "pkg" in this ACL2 session and that it
has since been undone, as by :ubt. Any future attempt in this
session to define "pkg" as a package must specify an identical
imports list.
The restriction stems from the need to implement the reinstallation
of saved logical worlds as in error recovery and the :oops command.
Suppose that the new defpkg attempts to import some symbol, a::sym,
not imported by the previous definition of "pkg". Because it was
not imported in the original package, the symbol pkg::sym, different
from a::sym, may well have been created and may well be used in some
saved worlds. Those saved worlds are Common Lisp objects being held
for you ``behind the scenes.'' In order to import a::sym into
"pkg" now we would have to unintern pkg::sym, rendering those
saved worlds ill-formed. It is because of saved worlds that we do
not actually clear out a package when it is undone.
At one point we thought it was sound to allow the new defpkg to
import a subset of the old. But that is incorrect. Suppose the old
definition of "pkg" imported a::sym but the new one does not.
Suppose we allowed that and implemented it simply by setting the
imports of "pkg" to the new subset. Then consider the conjecture
(eq a::sym pkg::sym). This ought not be a theorem because we did
not import a::sym into "pkg". But in fact in AKCL it is a theorem
because pkg::sym is read as a::sym because of the old imports.
printing the one-liner
Parent topic: MISCELLANEOUS Home
Examples: (assign print-doc-start-column nil) (assign print-doc-start-column 17)
This state global variable controls the column in which the
``one-liner'' of a formatted documentation string is printed.
Generally, when :doc is used to print a documentation string, the
name of the documented concept is printed and then :doc tabs over to
print-doc-start-column and prints the one-liner. If the name
extends past the desired column, :doc outputs a carriage return and
then tabs over to the column. If print-doc-start-column is nil,
:doc just starts the one-liner two spaces from the end of the name,
on the same line. The initial value of print-doc-start-column is
15.
the prompt printed by ld
Parent topic: MISCELLANEOUS Home
The prompt printed by ACL2 conveys information about various ``modes.'' See default-print-prompt and see ld-prompt for details.
a proof that e0-ord-< is well-founded on e0-ordinalps
Parent topic: MISCELLANEOUS Home
The soundness of ACL2 rests in part on the well-foundedness of
e0-ord-< on e0-ordinalps. This can be taken as obvious if one is
willing to grant that those concepts are simply encodings of the
standard mathematical notions of the ordinals below epsilon-0 and
its natural ordering relation. But it is possible to prove that
e0-ord-< is well-founded on e0-ordinalps without having to assert
any connection to the ordinals and that is what we do here.
We first observe three facts about e0-ord-< on ordinals that have
been proved by ACL2 using only structural induction on lists.
(defthm transitivity
(implies (and (e0-ordinalp x)
(e0-ordinalp y)
(e0-ordinalp z)
(e0-ord-< x y)
(e0-ord-< y z))
(e0-ord-< x z))
:rule-classes nil)
(defthm non-circularity
(implies (and (e0-ordinalp x)
(e0-ordinalp y)
(e0-ord-< x y))
(not (e0-ord-< y x)))
:rule-classes nil)
(defthm trichotomy
(implies (and (e0-ordinalp x)
(e0-ordinalp y))
(or (equal x y)
(e0-ord-< x y)
(e0-ord-< y x)))
:rule-classes nil)
These three properties establish that e0-ord-< orders the
e0-ordinalps. To put such a statement in the most standard
mathematical nomenclature, we can define the function:
(defun e0-ord-<= (x y) (or (equal x y) (e0-ord-< x y)))and then establish that
e0-ord-<= is a relation that is a simple,
complete (i.e., total) order on ordinals by the following three
lemmas, which have been proved:
(defthm antisymmetry
(implies (and (e0-ordinalp x)
(e0-ordinalp y)
(e0-ord-<= x y)
(e0-ord-<= y x))
(equal x y))
:rule-classes nil
:hints (("Goal" :use non-circularity)))
(defthm e0-ord-<=-transitivity
(implies (and (e0-ordinalp x)
(e0-ordinalp y)
(e0-ordinalp z)
(e0-ord-<= x y)
(e0-ord-<= y z))
(e0-ord-<= x z))
:rule-classes nil
:hints (("Goal" :use transitivity)))
(defthm trichotomy-of-e0-ord-<
(implies (and (e0-ordinalp x)
(e0-ordinalp y))
(or (e0-ord-<= x y)
(e0-ord-<= y x)))
:rule-classes nil
:hints (("Goal" :use trichotomy)))
Crucially important to the proof of the well-foundedness of
e0-ord-< on e0-ordinalps is the concept of ordinal-depth,
abbreviated od:
(defun od (l) (if (atom l) 0 (1+ (od (car l)))))If the
od of an e0-ordinalp x is smaller than that of an
e0-ordinalp y, then x is e0-ord-< y:
(defthm od-implies-ordlessp
(implies (and (e0-ordinalp x) (e0-ordinalp y)
(< (od x) (od y)))
(e0-ord-< x y)))
Remark. A consequence of this lemma is the fact that if s = s(1),
s(2), ... is an infinite, e0-ord-< descending sequence, then
od(s(1)), od(s(2)), ... is a ``weakly'' descending sequence of
non-negative integers: od(s(i)) is greater than or equal to
od(s(i+1)).
Lemma Main. For each non-negative integer n, e0-ord-< well-orders
the set of e0-ordinalps with od less than or equal to n .
Base Case. n = 0. The e0-ordinalps with 0 od are the non-negative integers. On the non-negative integers, e0-ord-< is the same as <.Theorem.Induction Step. n > 0. We assume that e0-ord-< well-orders the e0-ordinalps with od less than n.
If e0-ord-< does not well-order the e0-ordinalps with od less than or equal to n, we may let O be the e0-ord-<-least e0-ordinalp which is the car of the first member of an infinite, e0-ord-< descending sequence of e0-ordinalps of od less than or equal to n. The od of O is n-1.
Let k be the least integer > 0 such that for some infinite, e0-ord-< descending sequence s of e0-ordinalps with od less than or equal to n, the first element of s begins with k occurrences of O but not k+1 occurrences of O.
Having fixed O and k, let s = s(1), s(2), ... be an infinite, e0-ord-< descending sequence of e0-ordinalps with od less than or equal to n such that O occurs exactly k times at the beginning of s(1).
O occurs exactly k times at the beginning of each s(i). For suppose that s(j) is the first member of s with exactly m occurrences of O at the beginning, m /= k. If m = 0, then the first member of s(j) must be e0-ord-< O, contradicting the minimality of O. If 0 < m < k, then the fact that the sequence beginning at s(j) is infinitely descending contradicts the minimality of k. If m > k, then s(j) is greater than its predecessor, which has only k occurrences of O at the beginning; but this contradicts the fact that s is descending.
Let t = t(1), t(2), ... be the sequence of e0-ordinalps that is obtained by letting t(i) be the result of removing O from the front of s(i) exactly k times. t is infinitely descending. Furthermore, t(1) begins with an e0-ordinalp O' that is e0-ord-< O, and hence has od at most N-1 by the lemma od-implies-ordlessp. But this contradicts the minimality of O. Q.E.D.
e0-ord-< well-orders the e0-ordinalps. Proof. Every
infinite, e0-ord-< descending sequence of e0-ordinalps has the
property that each member has od less than or equal to the od, n, of
the first member of the sequence. This contradicts Lemma Main.
Q.E.D.
a predicate for recognizing term-like s-expressions
Parent topic: MISCELLANEOUS Home
Example Forms: (pseudo-termp '(car (cons x 'nil))) ; has value t (pseudo-termp '(car x y z)) ; also has value t! (pseudo-termp '(delta (h x))) ; has value t (pseudo-termp '(delta (h x) . 7)) ; has value nil (not a true-listp) (pseudo-termp '((lambda (x) (car x)) b)) ; has value t (pseudo-termp '(if x y 123)) ; has value nil (123 is not quoted) (pseudo-termp '(if x y '123)) ; has value tIf
x is the quotation of a term, then (pseudo-termp x) is t.
However, if x is not the quotation of a term it is not necessarily
the case that (pseudo-termp x) is nil.
See term for a discussion of the various meanings of the word
``term'' in ACL2. In its most strict sense, a term is either a
legal variable symbol, a quoted constant, or the application of an
n-ary function symbol or closed lambda-expression to n terms. By
``legal variable symbol'' we exclude constant symbols, such as t,
nil, and *ts-rational*. By ``quoted constants'' we include 't (aka
(quote t)), 'nil, '31, etc., and exclude constant names such as t,
nil and *ts-rational*, unquoted constants such as 31 or 1/2, and
ill-formed quote expressions such as (quote 3 4). By ``closed
lambda expression'' we exclude expressions, such as
(lambda (x) (cons x y)), containing free variables in their bodies.
Terms typed by the user are translated into strict terms for
internal use in ACL2.
The predicate termp checks this strict sense of ``term'' with
respect to a given ACL2 logical world; See world. Many ACL2
functions, such as the rewriter, require certain of their arguments
to satisfy termp. However, as of this writing, termp is in :program
mode and thus cannot be used effectively in conjectures to be
proved. Furthermore, if regarded simply from the perspective of an
effective guard for a term-processing function, termp checks many
irrelevant things. (Does it really matter that the variable symbols
encountered never start and end with an asterisk?) For these
reasons, we have introduced the notion of a ``pseudo-term'' and
embodied it in the predicate pseudo-termp, which is easier to
check, does not require the logical world as input, has :logic
mode, and is often perfectly suitable as a guard on term-processing
functions.
A pseudo-termp is either a symbol, a true list of length 2
beginning with the word quote, the application of an n-ary
pseudo-lambda expression to a true list of n pseudo-terms, or
the application of a symbol to a true list of n pseudo-termps.
By an ``n-ary pseudo-lambda expression'' we mean an expression
of the form (lambda (v1 ... vn) pterm), where the vi are
symbols (but not necessarily distinct legal variable symbols) and
pterm is a pseudo-termp.
Metafunctions may use pseudo-termp as a guard.
a common way to set ld-redefinition-action
Parent topic: MISCELLANEOUS Home
Example and General Form: ACL2 !>:redefThis command sets
ld-redefinition-action to '(:query . :overwrite).
As explained elsewhere (see ld-redefinition-action), this
allows redefinition of functions and other events without undoing.
A query will be made every time a redefinition is commanded; the
user must explicitly acknowledge that the redefinition is
intentional. It is possible to set ld-redefinition-action so that
the redefinition of non-system functions occurs quietly.
See ld-redefinition-action.
system hacker's redefinition command
Parent topic: MISCELLANEOUS Home
Example and General Form: ACL2 !>:redef! ACL2 p!>This command sets
ld-redefinition-action to '(:warn! . :overwrite)
and sets the default defun-mode to :program.
This is the ACL2 system hacker's redefinition command. Note that even system functions can be redefined with a mere warning. Be careful!
to collect the names that have been redefined
Parent topic: MISCELLANEOUS Home
Example and General Forms: (redefined-names state)
This function collects names that have been redefined in the current ACL2
state. :Program mode functions that were reclassified to
:logic functions are not collected, since such reclassification
cannot imperil soundness because it is allowed only when the new and old
definitions are identical.
Thus, if (redefined-names state) returns nil then no unsafe
definitions have been made, regardless of ld-redefinition-action.
See ld-redefinition-action.