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
(acl2-print-case), and may be set using the macro
set-acl2-print-case (which returns state), as follows.
:set-acl2-print-case :upcase ; Default printing
(set-acl2-print-case :upcase) ; Same as above
:set-acl2-print-case :downcase ; Print symbols in lower case when
; vertical bars are not required
(set-acl2-print-case :downcase) ; Same as above
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.