You can always use the Index icon below 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, runtime images of ACL2 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.
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 a very long book but we do not recommend that! See the ACL2 Home Page to download the Postscript.
Now let's continue with