		Search-engine friendly clone of the ACL2 documentation.

Pnumber-dot-digit

Pnumber-dot-digit->digit

Get the digit field from a pnumber-dot-digit.

Signature
(pnumber-dot-digit->digit x) → digit
Arguments: x — Guard (pnumberp x).
Returns: digit — Type (characterp digit).

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

Definitions and Theorems

Function: pnumber-dot-digit->digit$inline

(defun pnumber-dot-digit->digit$inline (x)
  (declare (xargs :guard (pnumberp x)))
  (declare (xargs :guard (equal (pnumber-kind x) :dot-digit)))
  (mbe :logic
       (b* ((x (and (equal (pnumber-kind x) :dot-digit)
                    x))
            (digit (acl2::char-fix (std::da-nth 0 (cdr x)))))
         (if (dec-digit-char-p digit) digit #\0))
       :exec (std::da-nth 0 (cdr x))))

Theorem: characterp-of-pnumber-dot-digit->digit

(defthm characterp-of-pnumber-dot-digit->digit
  (b* ((digit (pnumber-dot-digit->digit$inline x)))
    (characterp digit))
  :rule-classes :rewrite)

Theorem: pnumber-dot-digit->digit$inline-of-pnumber-fix-x

(defthm pnumber-dot-digit->digit$inline-of-pnumber-fix-x
  (equal (pnumber-dot-digit->digit$inline (pnumber-fix x))
         (pnumber-dot-digit->digit$inline x)))

Theorem: pnumber-dot-digit->digit$inline-pnumber-equiv-congruence-on-x

(defthm
      pnumber-dot-digit->digit$inline-pnumber-equiv-congruence-on-x
  (implies (pnumber-equiv x x-equiv)
           (equal (pnumber-dot-digit->digit$inline x)
                  (pnumber-dot-digit->digit$inline x-equiv)))
  :rule-classes :congruence)

Theorem: pnumber-dot-digit->digit-when-wrong-kind

(defthm pnumber-dot-digit->digit-when-wrong-kind
  (implies
       (not (equal (pnumber-kind x) :dot-digit))
       (equal (pnumber-dot-digit->digit x)
              (b* ((x nil)
                   (digit (acl2::char-fix (std::da-nth 0 (cdr x)))))
                (if (dec-digit-char-p digit)
                    digit
                  #\0)))))