		Search-engine friendly clone of the ACL2 documentation.

Oct-integer-literal

Oct-integer-literal->digits/uscores

Get the digits/uscores field from a oct-integer-literal.

Signature
(oct-integer-literal->digits/uscores x) → digits/uscores
Arguments: x — Guard (oct-integer-literalp x).
Returns: digits/uscores — Type (octdig/uscore-listp digits/uscores).

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

Definitions and Theorems

Function: oct-integer-literal->digits/uscores$inline

(defun oct-integer-literal->digits/uscores$inline (x)
 (declare (xargs :guard (oct-integer-literalp x)))
 (declare (xargs :guard t))
 (let ((__function__ 'oct-integer-literal->digits/uscores))
  (declare (ignorable __function__))
  (mbe
   :logic
   (b*
    ((x (and t x))
     (digits/uscores
          (octdig/uscore-list-fix (std::da-nth 0 (cdr x))))
     (prefix-upcase-p (acl2::bool-fix (std::da-nth 1 (cdr x))))
     (suffix?
        (optional-integer-type-suffix-fix (std::da-nth 2 (cdr x)))))
    (if (octdig/uscore-list-wfp digits/uscores)
        digits/uscores
      (list (octdig/uscore-digit (char-code #\0))
            (octdig/uscore-digit (char-code #\0)))))
   :exec (std::da-nth 0 (cdr x)))))

Theorem: octdig/uscore-listp-of-oct-integer-literal->digits/uscores

(defthm octdig/uscore-listp-of-oct-integer-literal->digits/uscores
  (b*
   ((digits/uscores (oct-integer-literal->digits/uscores$inline x)))
   (octdig/uscore-listp digits/uscores))
  :rule-classes :rewrite)

Theorem: oct-integer-literal->digits/uscores$inline-of-oct-integer-literal-fix-x

(defthm
 oct-integer-literal->digits/uscores$inline-of-oct-integer-literal-fix-x
 (equal (oct-integer-literal->digits/uscores$inline
             (oct-integer-literal-fix x))
        (oct-integer-literal->digits/uscores$inline x)))

Theorem: oct-integer-literal->digits/uscores$inline-oct-integer-literal-equiv-congruence-on-x

(defthm
 oct-integer-literal->digits/uscores$inline-oct-integer-literal-equiv-congruence-on-x
 (implies
      (oct-integer-literal-equiv x x-equiv)
      (equal (oct-integer-literal->digits/uscores$inline x)
             (oct-integer-literal->digits/uscores$inline x-equiv)))
 :rule-classes :congruence)