		Search-engine friendly clone of the ACL2 documentation.

Header-name-angles

Header-name-angles->chars

Get the chars field from a header-name-angles.

Signature
(header-name-angles->chars x) → chars
Arguments: x — Guard (header-namep x).
Returns: chars — Type (h-char-listp chars).

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

Definitions and Theorems

Function: header-name-angles->chars$inline

(defun header-name-angles->chars$inline (x)
  (declare (xargs :guard (header-namep x)))
  (declare (xargs :guard (equal (header-name-kind x) :angles)))
  (mbe :logic
       (b* ((x (and (equal (header-name-kind x) :angles)
                    x)))
         (h-char-list-fix (cdr x)))
       :exec (cdr x)))

Theorem: h-char-listp-of-header-name-angles->chars

(defthm h-char-listp-of-header-name-angles->chars
  (b* ((chars (header-name-angles->chars$inline x)))
    (h-char-listp chars))
  :rule-classes :rewrite)

Theorem: header-name-angles->chars$inline-of-header-name-fix-x

(defthm header-name-angles->chars$inline-of-header-name-fix-x
  (equal (header-name-angles->chars$inline (header-name-fix x))
         (header-name-angles->chars$inline x)))

Theorem: header-name-angles->chars$inline-header-name-equiv-congruence-on-x

(defthm
 header-name-angles->chars$inline-header-name-equiv-congruence-on-x
 (implies (header-name-equiv x x-equiv)
          (equal (header-name-angles->chars$inline x)
                 (header-name-angles->chars$inline x-equiv)))
 :rule-classes :congruence)

Theorem: header-name-angles->chars-when-wrong-kind

(defthm header-name-angles->chars-when-wrong-kind
  (implies (not (equal (header-name-kind x) :angles))
           (equal (header-name-angles->chars x)
                  (h-char-list-fix nil))))