		Search-engine friendly clone of the ACL2 documentation.

Pretty-printing-implementation

My-needs-slashes

Signature
(my-needs-slashes x config) → *
Arguments: x — Guard (stringp x).; config — Guard (printconfig-p config).

ACL2's similar function only checks whether we need symbols when print-escape or print-readably are set. I'm not going to bother with that, and just assume that we always want to escape symbols that need escaping.

Definitions and Theorems

Function: my-needs-slashes$inline

(defun my-needs-slashes$inline (x config)
  (declare (xargs :guard (and (stringp x)
                              (printconfig-p config))))
  (let ((acl2::__function__ 'my-needs-slashes))
    (declare (ignorable acl2::__function__))
    (acl2::may-need-slashes-fn x (printconfig->print-base config))))