Major Section: IO
By default, symbols are printed in upper case when vertical bars are
not required, as specified by Common Lisp. As with Common Lisp,
ACL2 supports printing in a "downcase" mode, where symbols are
printed in lower case. Many printing functions (some details below)
print characters in lower case for a symbol when the ACL2 state
global variable print-case has value :downcase and vertical bars
are not necessary for printing that symbol. (Thus, this state global
functions in complete analogy to the Common Lisp global *print-case*.)
The value print-case is returned by (print-case), and may be set
using the function set-print-case as follows.
(set-print-case :upcase state) ; Default printing
(set-print-case :downcase state) ; Print symbols in lower case when
; vertical bars are not required
The ACL2 user can expect that the :downcase setting will have an effect
for formatted output (see fmt and see fms) when the directives are ~p,
~P, ~q, or ~Q, for built-in functions princ$ and
prin1$, and the ppr family of functions, and not for built-in
function print-object$. For other printing functions, the effect of
:downcase is unspecified.
Also see print-control for other user-settable print controls.
