DEFDOC

add a documentation topic 
Major Section:  EVENTS


Examples:
(defdoc interp-section
   ":Doc-Section ...")


General Form:
(defdoc name doc-string)
where name is a symbol or string to be documented and doc-string is a documentation string (see doc-string). This event adds the documentation string for symbol name to the :doc data base. It may also be used to change the documentation for name if name already has documentation. The difference between this event and deflabel is that, unlike deflabel (but like table), it does not mark the current history with the name. But like deflabel, defdoc events are never considered redundant (see redundant-events).

See deflabel for a means of attaching a documentation string to a name that marks the current history with that name. We now elaborate further on how defdoc may be useful in place of deflabel.

It is usually sufficient to use deflabel when you might be tempted to use defdoc. However, unlike deflabel, defdoc does not mark the current history with name. Thus, defdoc is useful for introducing the documentation for a defun or deftheory event, for example, several events before the function or theory is actually defined.

For example, suppose you want to define a theory (using deftheory). You need to prove the lemmas in that theory before executing the deftheory event. However, it is quite natural to define a :doc-section (see doc-string) whose name is the name of the theory to be defined, and put the documentation for that theory's lemmas into that :doc-section. Defdoc is ideal for this purpose, since it can be used to introduce the :doc-section, followed by the lemmas referring to that :doc-section, and finally concluded with a deftheory event of the same name. If deflabel were used instead of defdoc, for example, then the deftheory event would be disallowed because the name is already in use by the deflabel event.

We also imagine that some users will want to use defdoc to insert the documentation for a function under development. This defdoc event would be followed by definitions of all the subroutines of that function, followed in turn by the function definition itself.

Any time defdoc is used to attach documentation to an already-documented name, the name must not be attached to a new :doc-section. We make this requirement as a way of avoiding loops in the documentation tree. When documentation is redefined, a warning will be printed to the terminal.