		Search-engine friendly clone of the ACL2 documentation.

Pnumber-number-nondigit

Pnumber-number-nondigit->nondigit

Get the nondigit field from a pnumber-number-nondigit.

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

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

Definitions and Theorems

Function: pnumber-number-nondigit->nondigit$inline

(defun pnumber-number-nondigit->nondigit$inline (x)
  (declare (xargs :guard (pnumberp x)))
  (declare (xargs :guard (equal (pnumber-kind x)
                                :number-nondigit)))
  (mbe :logic
       (b* ((x (and (equal (pnumber-kind x)
                           :number-nondigit)
                    x))
            (number (pnumber-fix (std::da-nth 0 (cdr x))))
            (nondigit (acl2::char-fix (std::da-nth 1 (cdr x)))))
         (if (str::letter/uscore-char-p nondigit)
             nondigit
           #\_))
       :exec (std::da-nth 1 (cdr x))))

Theorem: characterp-of-pnumber-number-nondigit->nondigit

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

Theorem: pnumber-number-nondigit->nondigit$inline-of-pnumber-fix-x

(defthm pnumber-number-nondigit->nondigit$inline-of-pnumber-fix-x
  (equal (pnumber-number-nondigit->nondigit$inline (pnumber-fix x))
         (pnumber-number-nondigit->nondigit$inline x)))

Theorem: pnumber-number-nondigit->nondigit$inline-pnumber-equiv-congruence-on-x

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

Theorem: pnumber-number-nondigit->nondigit-when-wrong-kind

(defthm pnumber-number-nondigit->nondigit-when-wrong-kind
 (implies
    (not (equal (pnumber-kind x)
                :number-nondigit))
    (equal (pnumber-number-nondigit->nondigit x)
           (b* ((x nil)
                (number (pnumber-fix (std::da-nth 0 (cdr x))))
                (nondigit (acl2::char-fix (std::da-nth 1 (cdr x)))))
             (if (str::letter/uscore-char-p nondigit)
                 nondigit
               #\_)))))