		Search-engine friendly clone of the ACL2 documentation.

Plexeme-punctuator

Plexeme-punctuator->punctuator

Get the punctuator field from a plexeme-punctuator.

Signature
(plexeme-punctuator->punctuator x) → punctuator
Arguments: x — Guard (plexemep x).
Returns: punctuator — Type (stringp punctuator).

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

Definitions and Theorems

Function: plexeme-punctuator->punctuator$inline

(defun plexeme-punctuator->punctuator$inline (x)
  (declare (xargs :guard (plexemep x)))
  (declare (xargs :guard (equal (plexeme-kind x) :punctuator)))
  (mbe :logic
       (b* ((x (and (equal (plexeme-kind x) :punctuator)
                    x)))
         (acl2::str-fix (std::da-nth 0 (cdr x))))
       :exec (std::da-nth 0 (cdr x))))

Theorem: stringp-of-plexeme-punctuator->punctuator

(defthm stringp-of-plexeme-punctuator->punctuator
  (b* ((punctuator (plexeme-punctuator->punctuator$inline x)))
    (stringp punctuator))
  :rule-classes :rewrite)

Theorem: plexeme-punctuator->punctuator$inline-of-plexeme-fix-x

(defthm plexeme-punctuator->punctuator$inline-of-plexeme-fix-x
  (equal (plexeme-punctuator->punctuator$inline (plexeme-fix x))
         (plexeme-punctuator->punctuator$inline x)))

Theorem: plexeme-punctuator->punctuator$inline-plexeme-equiv-congruence-on-x

(defthm
 plexeme-punctuator->punctuator$inline-plexeme-equiv-congruence-on-x
 (implies (plexeme-equiv x x-equiv)
          (equal (plexeme-punctuator->punctuator$inline x)
                 (plexeme-punctuator->punctuator$inline x-equiv)))
 :rule-classes :congruence)

Theorem: plexeme-punctuator->punctuator-when-wrong-kind

(defthm plexeme-punctuator->punctuator-when-wrong-kind
  (implies (not (equal (plexeme-kind x) :punctuator))
           (equal (plexeme-punctuator->punctuator x)
                  (acl2::str-fix nil))))