		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-standardp

Stringlit-standardp

Signature
(stringlit-standardp stringlit) → fty::result
Arguments: stringlit — Guard (stringlitp stringlit).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: stringlit-standardp

(defun stringlit-standardp (stringlit)
  (declare (xargs :guard (stringlitp stringlit)))
  (declare (ignorable stringlit))
  (let ((__function__ 'stringlit-standardp))
    (declare (ignorable __function__))
    (s-char-list-standardp (stringlit->schars stringlit))))

Theorem: booleanp-of-stringlit-standardp

(defthm booleanp-of-stringlit-standardp
  (b* ((fty::result (stringlit-standardp stringlit)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: stringlit-standardp-of-stringlit-fix-stringlit

(defthm stringlit-standardp-of-stringlit-fix-stringlit
  (equal (stringlit-standardp (stringlit-fix stringlit))
         (stringlit-standardp stringlit)))

Theorem: stringlit-standardp-stringlit-equiv-congruence-on-stringlit

(defthm stringlit-standardp-stringlit-equiv-congruence-on-stringlit
  (implies (stringlit-equiv stringlit stringlit-equiv)
           (equal (stringlit-standardp stringlit)
                  (stringlit-standardp stringlit-equiv)))
  :rule-classes :congruence)