Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

This FAQ is for people who've read through all the other sections of the tutorial introduction to the theorem prover (see introduction-to-the-theorem-prover and all the links from it that are not marked with the little warning sign (``''). Do not expect to understand our answers if you haven't taken the time to read through the tutorial. In the answers below you will see more links into the hypertext reference manual. While such links were marked ``'' in the tutorial, they are not marked that way here. When you enter the reference manual be prepared to explore and assemble a mini-course on the topic of interest, not a quick fix.

**Q**. How do I find something in the **ACL2 documentation**?
**A**. Try going to the Search link on the ACL2 home page.

**Q**. How does the theorem prover work? **A**. We really don't think you
need to know much about the inner workings of the prover to become an effective
user. That doesn't mean the system is self-explanatory! It means that stuff you
need to learn is not how the theorem prover works but how to interact with it!
That is what introduction-to-the-theorem-prover is about.
However, if you want the most basic overview of the prover, see architecture-of-the-prover.

**Q**. How do I **define a new function**?
**A**. See defun.

**Q**. How do I **define a new predicate**? **A**. See defun.

**Q**. How do I **define a new relation**? **A**. See defun.

**Q**. How do I define a **function or predicate that takes a varying number of arguments**?
**A**. You can't. However, see defmacro to learn
how to define a macro that takes a varying number of arguments and expands
into an arbitrary term that you compute.

**Q**. How do I define a **macro that is sensitive to the state**? **A**.
You can't. However, advanced users should consider `make-event`

.

**Q**. How do I define **mutually recursive** functions? **A**.
See mutual-recursion. However, you should realize that when two functions,
say `f`

and `g`

, are mutually recursive, properties of `f`

generally
have to be stated simultaneously with properties of `g`

, since inductive
proofs about one function require inductive hypotheses about the other.
Furthermore, ACL2 does not know how to do inductions for mutually recursive
functions and must be told. See mutual-recursion-proof-example.

**Q**. How do I declare the **type signature of a function**? **A**.
You can't. ACL2 is a syntactically untyped language and all functions are
defined on all objects in the ACL2 universe. We recommend that the new user
get used to this and only then explore the use of ACL2 to express and
enforce a type regime. In ACL2, the *guard* of a function is akin to the
type signature of a function in typed languages. However, ACL2 guards may
be arbitrary terms, not just type conditions, they only concern the inputs
to the function (not its result), and do not affect the axiom defining the
function -- all functions are defined on every combination of objects. You
may, of course, prove theorems that establish that every function called in
a definition or theorem is supplied with input satisfying its guards (which
necessarily involves describe the outputs too). These formulas are called
*guard conjectures* and the process of proving them is called *guard verification*.
Since guards are arbitrary ACL2 formulas, the ``type
regimes'' one tends to enforce in ACL2 can be much for flexible and
expressive than those in most programming languages. However, that
expressibility also means guard verification can be challenging
(indeed undecidable). On the other hand, if one limits oneself to simple
type-like guards, lemmas can be proved that make most guard verification
fully automatic and one can configure ACL2 to do guard verification
automatically at `defun`

-time. One may also delay guard verification
until ``the right'' lemmas have been proved. By doing guard verification
one can make functions execute faster by allowing the code to avoid runtime
checks. This is especially valuable to industrial users who have large
models used both in verification and as simulation engines for designed
artifacts. In addition, guard verification can give you the assurance that
you are using your functions within their intended domains and hence is a
form of functional specification and verification. However, all these
advantages aside, it is remarkably easy to drift away from the simplest type
regimes and write a guard that raises deep mathematical problems. New users
should not try to confront these problems until they are comfortable with
the theorem prover and with lemma development. Therefore, we **strongly**
recommend that you forget about types and guards and get used to reasoning
about total functions. When you do decide to learn about them, be prepared
for a complex story involving specification, execution efficiency,
and proof management. See guard.

**Q**. How do I tell `defun`

**what measure to use**?
**A**. See xargs, specifically `:measure`

.

**Q**. I specified a measure that always returns a natural number but ACL2
is acting like it's not a natural number. **A**. There are two likely problems.
The most likely one is that your measure isn't really always a natural!
Suppose the formals of your `defun`

are `x`

and `y`

and your measure
is `(m x y)`

. Suppose the recursive calls of your function are protected
by tests that insure that `x`

and `y`

are naturals. Then you might
assume `x`

and `y`

are naturals in the measure. But
ACL2 has to prove `(o-p (m x y))`

, where `o-p`

is the
predicate that recognizes ordinals (and naturals are ordinals). Note that the
theorem doesn't have any hypotheses! You might intuitively think that your measure
has to be an ordinal just under the conditions that lead to recursive calls. That's not
what ACL2 enforces. It has to be an ordinal, always. So you must change your
specified measure. For example, consider wrapping `nfix`

around it or around
its uses of `x`

and `y`

to coerce those quantities to naturals. The second most likely
explanation is that your measure returns a natural, always, but ACL2 doesn't know that and it
takes induction to prove. This might happen if `m`

involves some recursive functions.
In this case, prove `(natp (m x y))`

before your `defun`

. Perhaps you should
consider making the `natp`

lemma a `:`

`type-prescription`

lemma to make ACL2's
typing algorithm aware of it.

**Q**. How do I tell `defun`

**what well-founded relation to use**?
**A**. See xargs, specifically `:well-founded-relation`

.

**Q**. How do I show that a **relation is well-founded**?
**A**. Prove a theorem establishing that there is an order preserving embedding into the
ordinals and store it with `:rule-classes`

`:`

`well-founded-relation`

.

**Q**. What is an **ordinal**? What does it mean to be
**well-founded**? **A**. Ordinals are an extension of the natural
numbers used to insure that a process can't go on forever. Like naturals,
they can be added, multiplied, and exponentiated. There is a sense of one
ordinal being less than another. Unlike the naturals, each of which is
finite, the ordinals include infinite objects. Now imagine ``standing'' on
an ordinal and ``stepping'' to a smaller one. Like the naturals, this
``walk down the ordinals'' can't go on forever, even if you start on an
infinite ordinal. That is because the ordinals are *well-founded*. See
`o-p`

for more information about ordinals in ACL2 and about
well-foundedness. See ordinals for a deeper discussion and a discussion of
books that can help configure ACL2 to reason about ordinals.

**Q**. How can provide **hints for the termination proofs** in `defun`

?
**A**. See xargs, specifically `:hints`

(for the termination proofs) and
`:guard-hints`

(for the guard verification proofs).

**Q**. How do I define a **constant** (something like a **global variable**)?
**A**. See defconst. But remember that as an applicative
programming language, ACL2 does not have global variables! You can define a
symbol to have a fixed value and use the symbol sort of like a global
variable in function definitions: you may refer to the value of the symbol
in your functions without passing the variable in as formal parameter. But
you may not ever change the value of the symbol!

**Q**. How do I save the value of a top-level computation for future use?
**A**. See assign and see @.

**Q**. How do I introduce **new syntactic form** or **abbreviation**?
**A**. See defmacro.

**Q**. How can create and modify an array? **A**. ACL2 is a functional
language, so it is impossible to destructively modify an existing object;
technically, all ``updates'' to objects must be implemented by ``copy-on-write''
semantics. That said, ACL2 provides support for arrays, provided you
use them in a restricted way. They give you constant-time access and
change under the use restrictions.

**Q**. How do I read from or write to a file? How do I do IO? **A**.
To manipulate files, your function must have `state`

as an argument, so
you should read about the restrictions that imposes. For input/output
facilities, see io.

**Q**. How do I define a **structure that can be destructively modified**?
**A**. ACL2 is an *applicative programming language*. You can't modify
objects arbitrarily! You basically have to ``copy on write,'' which means
you construct new objects from old ones, making the changes you want in the
new one. If the `car`

of some object is `1`

at one moment and `2`

later, then the basic logical axiom `(car x)`

= `(car x)`

is violated!
However, if the only reference to the old object, e.g., *x*, was to pass
it to the code that copied and ``changed'' it, then ACL2 can re-use the old
object to produce the new one and the axioms would not object. Such
syntactic restrictions can make *x* a modifiable structure but they will
impose a heavy burden on you as a programmer: if pass such an *x* to a
function and the function modifies it, then you must pass *x* only to that
function and you must return the modified value and use it henceforth. Such
objects are said to be *single threaded*. See defstobj.

**Q**. How do I write a universal quantifier? An existential quantifier?
How can I say ``for all'' or ``there exists''? **A** You can't literally
write quantifiers. But ACL2 has the power of full first order logic with
quantification. See quantifiers.

**Q**. How do I introduce an undefined or uninterpreted function symbol?
Can I constrain it to have certain properties? **A**. See encapsulate.

**Q**. How can I hide a lemma? I want to prove a lemma temporarily
to use in another proof but I don't want the lemma around thereafter.
**A**. One way to get a similar effect is to prove the lemma and then
disable it with an `(in-theory (disable ...))`

event; see in-theory.
Another way is to put the lemma and the theorem that needs it into an
`encapsulate`

and wrap a `local`

around the lemma.

**Q**. What is an **event**? **A**. An *event* is a command that adds
information to the ACL2 database (the ``logical world''), like `defun`

or
`defthm`

. See events.

**Q**. How do I say that I **do not want a rewrite rule** generated from a
theorem? **A**. The command

(defthmwill attempt to provenameformula:rule-classes nil)

**Q**. How do I say that I want a formula to be **stored as a rewrite rule**?
**A**. The command

(defthmwill attempt to provenameformula)

`(:rewrite `

`AND`

. In
this case, each conjunctive branch through the conclusion generates a rule
named `(:rewrite `

` . i)`

, for
**Q**. How do I say that I want a formula to be **stored as a rewrite rule**
**and some other kinds of rules**? **A**. The command

(defthmwill attempt to provenameformula:rule-classes (:class1...classk))

`:REWRITE`

or `:GENERALIZE`

, naming a rule class (see rule-classes), or
else should be a list that starts with a rule class and then lists the
relevant modifiers. Be sure to include `:REWRITE`

among the rule classes
if you want the formula to generate a rewrite rule. It doesn't do that
automatically if you explicitly specify `:rule-classes`

!
**Q**. How do I **rearrange** the shape of a formula before generating a
rule from it? **A**. See rule-classes and read about the `:corollary`

modifier.

**Q**. What is a **type-prescription**? **A**. ACL2 has an algorithm for
determining the type of object returned by a term, where a type is one of the Common Lisp
primitive datatypes such as natural, integer, Boolean, cons, true-listp, etc.
Rules provided by you can influence this algorithm. See type-prescription.

**Q**. How do **rewrite rules work**? **A**. Re-read the tutorial
sections: introduction-to-rewrite-rules-part-1 and
introduction-to-rewrite-rules-part-2.

**Q**. How do I **see what's in the database**? **A**. You can't look at
the entire database with user-friendly tools. You can print the command
that introduced a particular name, print the entire sequence of user
commands, print the commands in the region between two commands, print all
the rewrite rules that apply to a given term or function symbol, and many
other options. See history. If you have loaded a book from another user,
you might wish to read the source file. For example, the source file for
`(include-book "arithmetic-5/top" :dir :system)`

is the file named
`arithmetic-5/top.lisp`

on the `acl2-sources/books/`

directory where
ever your ACL2 sources are installed. Often, books are well-documented by
comments by their authors. Some books have `Readme`

or `README`

files
on the same directory.

**Q**. How do I **undo** a command? **A**. See history, especially
see u (``undo'') and see ubt (``undo back through''). **Q**. What
**rewrite rules match** a given term? **A**. See pl.

**Q**. What were those **questions to ask when looking at key checkpoints**?
**A**. See introduction-to-key-checkpoints.

**Q**. How do I figure out **why a rewrite rule won't fire**? **A**. If you
activate rewrite rule monitoring (see brr) and then install a
monitor (see monitor) on the rule in question, ACL2 will enter an
interactive break whenever the pattern of the rule is matched against a
target in a proof. So after installing the monitor, re-try the proof and
then interact with the rewriter via break commands (see brr-commands).
Like all trace and break packages, you have to know what you're doing to use
the break rewrite facility, so read the material in the reference manual.
If no interactive break happens after you've installed the monitor on your
rule and re-tried the proof, it means no suitable target ever arose. Don't
forget to turn off monitoring when you're done as it slows down the system.

**Q**. **Why is a proof taking so long?** **A**. Unexpectedly poor
performance on simple problems is usually a sign of cyclic rewriting or
combinatoric explosion. See dmr and see accumulated-persistence.

**Q**. How do I tell ACL2 **what induction to do** for a particular
formula? **A**. When issuing the `defthm`

command for the formula, supply
an `:induct`

hint:

(defthmwherenameformula:hints (("Goal" :induct (f x1 ... xn))))

`f`

is a function that recurs the way you want the induction to
unfold and `x1 ... xn`

are the relevant variables in `f`

appropriately for each formula that needs an
induct hint, though sometimes you can re-use an earlier `f`

or one of the
functions in the formula itself. It doesn't matter what value `(f x1 ... xn)`

returns. All that matters is how it recurs. The termination
analysis for `f`

justifies the induction done. See hints, especially the
section on `:induct`

hints; also see induction.
**Q**. ACL2 doesn't know **simple arithmetic** that can simplify the term
`(+ 1 -1 x)`

. **A**. You should load an arithmetic book whenever you're dealing
with an arithmetic problem. The simplest arithmetic book is loaded with the
event `(include-book "arithmetic/top-with-meta" :dir :system)`

. If
you're using `floor`

and `mod`

or non-linear arithmetic like `(* x y)`

you should use `(include-book "arithmetic-5/top" :dir :system)`

. See
also the discussion of arithmetic books under the ``Lemma Libraries and
Utilities'' link of the ACL2 home page.

**Q**. ACL2 is not using an **arithmetic lemma** that I proved.
**A**. Lemmas concluding with arithmetic inequalities, like

(implies (member e x) (< (len (delete e x)) (len x)))are not good rewrite rules because they rarely match targets because of intervening arithmetic operators. For example, the above conclusion doesn't match

`(< (LEN (DELETE E X)) (+ 1 (LEN X)))`

. You should store such lemmas as
`:linear`

rules by using the command:
(defthm len-delete (implies (member e x) (< (len (delete e x)) (len x))) :rule-classes :linear)See linear.

**Q**. What is a **linear rule**?
**A**. See linear.

**Q**. How do I make ACL2 **treat a relation as an equality**? **A**. We
assume you mean to treat the relation as an equivalence, i.e., replace one
term by another when they are equivalent under your relation.
See equivalence, see congruence, and see refinement.

**Q**. One of my rewrite rules has a **hypothesis that doesn't rewrite**
to true. What do I do? **A**. Prove a rewrite rule that establishes that
hypothesis under the relevant assumptions from the context of the intended
target. Alternatively, undo the rule and restate it with a `force`

around the problematic hypothesis, making ACL2 assume the hypothesis when
the rule is applied and raising the truth of the hypothesis as an explicit
subgoal of the proof. See also `case-split`

. Of course, you should
always state the strongest rewrite rules you can think of, eliminating hypotheses
or shifting them to the right-hand side inside of `IF`

s; see strong-rewrite-rules.

**Q**. How do I make ACL2 ``guess'' the **right instantiation of a free variable**?
**A**. You can provide a `:restrict`

hint that names the problematic
lemma and provides an instantiation of the free variable. See hints,
specifically `:restrict`

. You could alternatively give a hint that
`:uses`

the rule and provides the appropriate instantiation in full.
See hints, specifically `:use`

. Recall that ACL2 guesses free variable
instantiations by matching the problematic hypothesis to the assumptions in
the context of the target. If the appropriate assumption is present but
ACL2 is finding another one, try undoing the problematic rule and proving it
again, specifying the `:match-free :all`

modifier of the `:rewrite`

or
`:linear`

rule class. See rule-classes. Alternativey, undo and prove the
problematic rule again and use a `bind-free`

form to compute the
appropriate instantiation.

**Q**. How can I make ACL2 do a **case split** to prove a certain subgoal?
**A**. See hints, specifically `:cases`

.

**Q**. How can I **prevent ACL2 from using a rewrite rule**? **A**.
See hints, specifically `:in-theory (disable ...)`

. If the use of the
rule is problematic in only one subgoal and the lemma is needed in other subgoals,
disable the lemma only in the problematic subgoal by specifying the subgoal name (e.g.,
`"Subgoal 1/3.2.1"`

) as the goal specifier in the hint. If the rule
isn't needed anywhere in the proof, you could use the specifier
`"Goal"`

. If you don't think the rule will ever be needed for a while,
you could globally disable it with the event `(in-theory (disable ...))`

(see in-theory) executed before the first problematic proof. If the
rule has never been used or must always be disabled, undo it and prove it
again with `:`

`rule-classes`

`nil`

.

**Q**. How can I prevent ACL2 from running a definition on constants?
I tried disabling the function but that didn't work. **A**.
If you have a function named `f`

then disabling `f`

will disable the
definitional axiom about `f`

. But ACL2 has another kind of rule about
`f`

, telling it how to evaluate `f`

. The rune of this rule is
`(:executable-counterpart f)`

. Try disabling that, as in the `:`

`hints`

`((`

...
`:in-theory (disable (:executable-counterpart f)) ...c[))`

.

**Q**. How can I make ACL2 **use a rule** in a proof?
**A**. See hints, specifically `:use`

.

**Q**. How can I make ACL2 expand a function call in a proof?
**A**. You can give an `:`

See expand hint.

**Q**. ACL2 sometimes aborts the proof attempt before showing me all of the
subgoals. How can I make it just keep going instead of aborting early?
**A**. See otf-flg, which stands for Onward Thru the Fog FLaG.

**Q**. How can I **compute when I want a rule to fire**? **A**.
See syntaxp.

**Q**. How can I add **pragmatic advice to a lemma after it has been proved**?
For example, how can add a forced hypothesis, a backchain limit, or a
`syntaxp`

test? **A**. You can't. You can undo the lemma, restate it
appropriately, and prove it again. This produces the cleanest database.
Alternatively, you can prove the restated lemma under a new name -- a
task that should be easy since the old version is in the database and will
presumably make the proof trivial -- and then disable the old name.

**Q**. How can I **stop ACL2 from rewriting a term**? **A**. If you need
rewriting done but want to prevent some particular terms from being
rewritten, see hints, specifically `:hands-off`

. Alternatively, consider
embedding the problematic term in a `hide`

. Users sometime develop
special theories (see theory) containing just the rules they want and
then use hints to switch to those theories on the appropriate subgoals.

**Q**. Can I **compute which subgoals a hint refers to**?
**A**. Yes, see computed-hints. This topic is for advanced users but knowing
that it is possible might come in handy someday.

**Q**. I want the rewriter to **always use one theory and then switch to another** so that
it doesn't use my most complicated before until doing the simple things.
**A**. This is possible but is something for the advanced user. It can be done
using a form of computed-hints. See using-computed-hints-7.

**Q**. Is there a way to attach **the same hint to every defthm**?
**A**. See default-hints.

**Q**. How can I just tell ACL2 the proof steps? **A**. See verify and
see proof-checker.

**Q**. How can I write **my own simplifier**?
**A**. See meta.

**Q**. How can I add an axiom or just assume some lemma without proof?
**A**. This is very dangerous but is a good strategy for exploring whether or
not a certain set of lemmas (and their rules) is sufficient to prove your goal.
See defaxiom and see skip-proofs.

**Q**. How can redefine a user-defined function? **A**. This is tricky. What if
you've already proved theorems about the old definition and then wish to change it?
There are several options. See ld-redefinition-action (and note specifically the
discussion of updater function for it, `set-ld-redefinition-action`

); also
see redef, see redef!, see redef+, and see redef-.

**Q**. How do I **change a function from** `:program`

**mode to**
`:logic`

**mode**? **A**. See verify-termination.

**Q**. How do I **change the guards** on a function? **A**. You can't.
Undo it and redefine it.

**Q**. What is **program mode**?
**A**. See program.

**Q**. What does the ACL2 **prompt** mean? **A**.
See introduction-to-a-few-system-considerations or, specifically, see prompt.

**Q**. What is **logic mode**?
**A**. See logic.

**Q**. How do I **get into or out of** `:program`

**mode?** `:Logic`

**mode?** **A**. See program and see logic. You can enter these modes
temporarily for a particular `defun`

by using
`(declare (xargs :mode :program))`

or `(declare (xargs :mode :logic))`

after the list of formal parameters to the definition.

**Q**. How do I quit from ACL2? **A**. This varies depending on the
interface you're using. See introduction-to-a-few-system-considerations.

**Q**. How do I **load a file** of definitions and theorems created by
someone else? **A**. See include-book.

**Q**. How do I **create my own book** of definitions and theorems?
**A**. See books.

**Q**. Where are the ``distributed books'' referenced by **:dir :system**
on my machine? **A**. If your ACL2 is installed on the directory
*dir*`/acl2-sources`

, then the distributed books are the files under the
directory *dir*`/acl2-sources/books/`

.

**Q**. How can I find out **what books are available**? **A**. Go to the
ACL2 home page, `http://www.cs.utexas.edu/u/moore/acl2/`

and look at the
link labeled ``Lemma Libraries and Utilities.''

**Q**. How do I **produce my own book**?
**A**. See books.

**Q**. What is a **decision procedure**? What **decision procedures does ACL2 have**?
**A**. A *decision procedure* is an algorithm that given
enough time and space can determine, for all the formulas in a certain
syntactic class of formulas, whether the formula is a theorem or not. The
most well-known decision procedure is for propositional calculus: by testing
a formula under all the combinations Boolean assignments to the variables,
one can decide if a propositional formula is a theorem. The syntactic class
consists of all formulas you can write using just variables, constants, and
compositions of the functions `and`

, `or`

, `not`

, `implies`

,
`iff`

, and `if`

. There are, of course, an exponential number of
different assignments so the algorithm can be slow. ACL2 contains a
propositional decision procedure based on symbolic normalization that can be
faster than trying all the combinations of truthvalues -- but is not
guaranteed to be faster. ACL2 also contains an optional bdd procedure.
ACL2 also contains a decision procedure for rational arithmetic involving
variables, rational constants, addition, multiplication by rational
constants, equality, and the various versions of arithmetic
inequality (`<`

, `<=`

, `>=`

, and `>`

). It can be extended with
`:`

`linear`

lemmas. ACL2 is complete for equality over
uninterpreted (e.g., undefined and unconstrained) function symbols using an
algorithm based on transitive closure of equivalence classes under
functional substitutivity. Finally, you can make ACL2 use other decision
procedures, even ones implemented outside of ACL2; see clause-processor.

**Q**. ACL2 has the **change of variable** trick (**destructor elimination**)
that it does to get rid of `(CAR X)`

and `(CDR X)`

by
replacing `x`

by `(CONS A B)`

. Is there a way to make ACL2 do that for
other terms? **A**. Yes. See elim.

**Q**. How can I **prevent destructor elimination**?
**A**. See hints, specifically `:do-not '(eliminate-destructors)`

.

**Q**. How can I **prevent cross-fertilization**?
**A**. See hints, specifically `:do-not '(fertilize)`

.

**Q**. How can I **prevent generalization**?
**A**. See hints, specifically `:do-not '(generalize)`

.

**Q**. How can I make ACL2 **impose a restriction on a new variable**
introduced by destructor elimination or generalization? **A**.
See generalize.

**Q**. What **rule classes** are there?
**A**. See rule-classes.

**Q**. What is a **theory**?
**A**. See theories.

**Q**. How are **hints inherited by the children of a subgoal**?
**A**. See hints-and-the-waterfall.

**Q**. How do I use ACL2 under **Emacs**? **A**. See emacs.

**Q**. How do I use ACL2 under **Eclipse**? **A**. See ACL2-Sedan.

**Q**. How do I interrupt the prover?
**A**. The keyboard sequence for interrupting a running process depends your
operating system, host Common Lisp, and user interface (e.g., Emacs, Eclipse, etc.).
But perhaps a few examples will help you discover what you need to know.
If your host Common Lisp is GCL or Allegro and you are typing
directly to the Common Lisp process, then you can interrupt a computation by
typing ``ctrl-c'' (hold down the Control key and hit the ``c'' key once).
But other Lisps may require some other control sequence. If you are typing
to an Emacs process which is running the GCL or Allegro Common Lisp process
in a shell buffer, you should type ctrl-c ctrl-c -- that is, you have to type the
previously mentioned sequence twice in succession. If you are running the
ACL2 Sedan, you can use the *Interrupt Session* button on the tool bar.
The environment you enter when you interrupt depends on various factors and
basically you should endeavor to get back to the top level ACL2 command
loop, perhaps by typing some kind of Lisp depenent ``abort'' command like
`A`

or `:q`

, or `:abort!`

. You can usually determine what environment
you're in by paying attention to the prompt.

**Q**. What is the **ACL2 loop**? **A**. That is the name given to the
interactive environment ACL2 provides, a ``read-eval-print loop'' in which
the user submits successive commands by typing ACL2 expressions and keyword
commands. See introduction-to-a-few-system-considerations.

**Q**. What is **raw lisp**? **A**. That is our name for the host
Common Lisp in which ACL2 is implemented.
See introduction-to-a-few-system-considerations. There is an ACL2 mode
named *raw mode* which is different from ``raw lisp.'' See set-raw-mode.

**Q**. Can I get a tree-like view of a proof? **A**. See proof-tree for an
Emacs utility that displays proof trees and allows you to navigate through a proof
from the proof tree. The ACL2 Sedan also supports proof trees and you should see
the ACL2s documention on that topic.

**Q**. I used the earlier Boyer-Moore theorem prover, Nqthm. How is
ACL2 different? **A**. See nqthm-to-acl2.

If you are reading this as part of the tutorial introduction to the theorem
prover, use your browser's **Back Button** now to return to
introduction-to-the-theorem-prover.