		Search-engine friendly clone of the ACL2 documentation.

Atj-test-value

Atj-test-value-kind

Get the kind (tag) of a atj-test-value structure.

Signature
(atj-test-value-kind x) → kind
Arguments: x — Guard (atj-test-valuep x).

Definitions and Theorems

Function: atj-test-value-kind$inline

(defun atj-test-value-kind$inline (x)
  (declare (xargs :guard (atj-test-valuep x)))
  (let ((__function__ 'atj-test-value-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :acl2)) :acl2)
                      ((eq (car x) :jboolean) :jboolean)
                      ((eq (car x) :jchar) :jchar)
                      ((eq (car x) :jbyte) :jbyte)
                      ((eq (car x) :jshort) :jshort)
                      ((eq (car x) :jint) :jint)
                      ((eq (car x) :jlong) :jlong)
                      ((eq (car x) :jboolean[]) :jboolean[])
                      ((eq (car x) :jchar[]) :jchar[])
                      ((eq (car x) :jbyte[]) :jbyte[])
                      ((eq (car x) :jshort[]) :jshort[])
                      ((eq (car x) :jint[]) :jint[])
                      (t :jlong[]))
         :exec (car x))))

Theorem: atj-test-value-kind-possibilities

(defthm atj-test-value-kind-possibilities
  (or (equal (atj-test-value-kind x) :acl2)
      (equal (atj-test-value-kind x)
             :jboolean)
      (equal (atj-test-value-kind x) :jchar)
      (equal (atj-test-value-kind x) :jbyte)
      (equal (atj-test-value-kind x) :jshort)
      (equal (atj-test-value-kind x) :jint)
      (equal (atj-test-value-kind x) :jlong)
      (equal (atj-test-value-kind x)
             :jboolean[])
      (equal (atj-test-value-kind x) :jchar[])
      (equal (atj-test-value-kind x) :jbyte[])
      (equal (atj-test-value-kind x)
             :jshort[])
      (equal (atj-test-value-kind x) :jint[])
      (equal (atj-test-value-kind x)
             :jlong[]))
  :rule-classes
  ((:forward-chaining :trigger-terms ((atj-test-value-kind x)))))