|
|
|---|
|
|
|
|---|
A simple macro for easing the documentation process
The def::doc macro eases the process of constructing documentation strings for ACL2 symbols. See doc. Macro keywords are used to identify content for each of the primary documentation elements:
:section Either a symbol or string identifying the section :one-liner A simple one-line overview of the symbol :notes Notes related to this symbol :details Documentation details about the symbol
The string arguments used by the macro can be computed, allowing the user to
use functions as abbreviations for common and unwieldly documentation
constructs.