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 (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.