		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Check-literal-is-string-literal

Check if a literal is a string literal, returning its list of characters if successful.

Signature
(check-literal-is-string-literal lit) → chars
Arguments: lit — Guard (literalp lit).
Returns: chars — Type (char-list-resultp chars).

Definitions and Theorems

Function: check-literal-is-string-literal

(defun check-literal-is-string-literal (lit)
  (declare (xargs :guard (literalp lit)))
  (let ((__function__ 'check-literal-is-string-literal))
    (declare (ignorable __function__))
    (case (literal-kind lit)
      (:string (literal-string->get lit))
      (t (reserrf (list :found (literal-fix lit)))))))

Theorem: char-list-resultp-of-check-literal-is-string-literal

(defthm char-list-resultp-of-check-literal-is-string-literal
  (b* ((chars (check-literal-is-string-literal lit)))
    (char-list-resultp chars))
  :rule-classes :rewrite)

Theorem: check-literal-is-string-literal-of-literal-fix-lit

(defthm check-literal-is-string-literal-of-literal-fix-lit
  (equal (check-literal-is-string-literal (literal-fix lit))
         (check-literal-is-string-literal lit)))

Theorem: check-literal-is-string-literal-literal-equiv-congruence-on-lit

(defthm
    check-literal-is-string-literal-literal-equiv-congruence-on-lit
  (implies (literal-equiv lit lit-equiv)
           (equal (check-literal-is-string-literal lit)
                  (check-literal-is-string-literal lit-equiv)))
  :rule-classes :congruence)