## How To Find Out about ACL2 Functions (continued)

You can always use the Index to find the documentation of
functions. Try it. Click on the Index icon below. Then use the
Find command of your browser to find ``endp'' in that document and
follow the link. But remember to come back here.

The ACL2 documentation is also available via Emacs' TexInfo, allowing
you to explore the hyperlinked documentation in the comfort of a text
editor that can also interact with ACL2.

In addition, some runtime images of ACL2 (the so-called ``large
image'') have the hyperlinked text as a large ACL2 data structure
that can be explored with ACL2's **:doc** command. If you have ACL2
running, try the command **:doc endp**. If that doesn't work, you
are running the ``small image.''

Another way to find out about ACL2 functions, if you have an ACL2
image available, is to use the command :`args`

which
prints the formals, type, and guard of a function symbol.

Of course, the ACL2 documentation can also be printed out as 700 page
book. See the ACL2 Home Page to download the Postscript.

Now let's continue with `app`

.