		Search-engine friendly clone of the ACL2 documentation.

Pnumber

Pnumber-kind

Get the kind (tag) of a pnumber structure.

Signature
(pnumber-kind x) → kind
Arguments: x — Guard (pnumberp x).

Definitions and Theorems

Function: pnumber-kind$inline

(defun pnumber-kind$inline (x)
  (declare (xargs :guard (pnumberp x)))
  (mbe :logic (cond ((or (atom x) (eq (car x) :digit))
                     :digit)
                    ((eq (car x) :dot-digit) :dot-digit)
                    ((eq (car x) :number-digit)
                     :number-digit)
                    ((eq (car x) :number-nondigit)
                     :number-nondigit)
                    ((eq (car x) :number-locase-e-sign)
                     :number-locase-e-sign)
                    ((eq (car x) :number-upcase-e-sign)
                     :number-upcase-e-sign)
                    ((eq (car x) :number-locase-p-sign)
                     :number-locase-p-sign)
                    ((eq (car x) :number-upcase-p-sign)
                     :number-upcase-p-sign)
                    (t :number-dot))
       :exec (car x)))

Theorem: pnumber-kind-possibilities

(defthm pnumber-kind-possibilities
  (or (equal (pnumber-kind x) :digit)
      (equal (pnumber-kind x) :dot-digit)
      (equal (pnumber-kind x) :number-digit)
      (equal (pnumber-kind x)
             :number-nondigit)
      (equal (pnumber-kind x)
             :number-locase-e-sign)
      (equal (pnumber-kind x)
             :number-upcase-e-sign)
      (equal (pnumber-kind x)
             :number-locase-p-sign)
      (equal (pnumber-kind x)
             :number-upcase-p-sign)
      (equal (pnumber-kind x) :number-dot))
  :rule-classes
  ((:forward-chaining :trigger-terms ((pnumber-kind x)))))