		Search-engine friendly clone of the ACL2 documentation.

Constructor-preliminaries

String-downcase$

A variant of common-lisp::string-downcase applicable to any string.

The built-in common-lisp::string-downcase has a guard requiring all the characters in the string to be standard. This function ``totalizes'' common-lisp::string-downcase to all strings by checking whether all the characters in the string are standard, and by throwing a hard error if any of them is not.

This facilitates guard verification of code involving this function. The hard error seems appropriate for the envisioned usage of this function within the XDOC constructors, meant to be called to produce XDOC strings during book certification.

Definitions and Theorems

Function: string-downcase$

(defun string-downcase$ (string)
  (declare (xargs :guard (stringp string)))
  (if (standard-char-listp (coerce string 'list))
      (common-lisp::string-downcase string)
    (prog2$ (er hard? 'string-downcase$
                "Attempt to downcase non-standard string ~x0."
                string)
            "")))

Theorem: stringp-of-string-downcase$

(defthm stringp-of-string-downcase$
  (stringp (string-downcase$ string)))