		Search-engine friendly clone of the ACL2 documentation.

Stringlit

Stringlit->prefix?

Get the prefix? field from a stringlit.

Signature
(stringlit->prefix? x) → prefix?
Arguments: x — Guard (stringlitp x).
Returns: prefix? — Type (eprefix-optionp prefix?).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: stringlit->prefix?$inline

(defun stringlit->prefix?$inline (x)
  (declare (xargs :guard (stringlitp x)))
  (declare (xargs :guard t))
  (let ((__function__ 'stringlit->prefix?))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and t x)))
           (eprefix-option-fix (cdr (std::da-nth 0 x))))
         :exec (cdr (std::da-nth 0 x)))))

Theorem: eprefix-optionp-of-stringlit->prefix?

(defthm eprefix-optionp-of-stringlit->prefix?
  (b* ((prefix? (stringlit->prefix?$inline x)))
    (eprefix-optionp prefix?))
  :rule-classes :rewrite)

Theorem: stringlit->prefix?$inline-of-stringlit-fix-x

(defthm stringlit->prefix?$inline-of-stringlit-fix-x
  (equal (stringlit->prefix?$inline (stringlit-fix x))
         (stringlit->prefix?$inline x)))

Theorem: stringlit->prefix?$inline-stringlit-equiv-congruence-on-x

(defthm stringlit->prefix?$inline-stringlit-equiv-congruence-on-x
  (implies (stringlit-equiv x x-equiv)
           (equal (stringlit->prefix?$inline x)
                  (stringlit->prefix?$inline x-equiv)))
  :rule-classes :congruence)