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.
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.
