control whether symbols are printed in upper case or in lower case
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.