		Search-engine friendly clone of the ACL2 documentation.

Set-print-case

Control whether symbols are printed in upper case or in lower case

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 ~x, ~X, ~y, or ~Y, 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.