ATJ type of an ATJ test value.
(atj-test-value-to-type test-value) → type
Function:
(defun atj-test-value-to-type (test-value) (declare (xargs :guard (atj-test-valuep test-value))) (let ((__function__ 'atj-test-value-to-type)) (declare (ignorable __function__)) (atj-test-value-case test-value :acl2 (atj-type-of-value test-value.get) :jboolean (atj-type-jprim (primitive-type-boolean)) :jchar (atj-type-jprim (primitive-type-char)) :jbyte (atj-type-jprim (primitive-type-byte)) :jshort (atj-type-jprim (primitive-type-short)) :jint (atj-type-jprim (primitive-type-int)) :jlong (atj-type-jprim (primitive-type-long)) :jboolean[] (atj-type-jprimarr (primitive-type-boolean)) :jchar[] (atj-type-jprimarr (primitive-type-char)) :jbyte[] (atj-type-jprimarr (primitive-type-byte)) :jshort[] (atj-type-jprimarr (primitive-type-short)) :jint[] (atj-type-jprimarr (primitive-type-int)) :jlong[] (atj-type-jprimarr (primitive-type-long)))))
Theorem:
(defthm atj-typep-of-atj-test-value-to-type (b* ((type (atj-test-value-to-type test-value))) (atj-typep type)) :rule-classes :rewrite)
Theorem:
(defthm atj-test-value-to-type-of-atj-test-value-fix-test-value (equal (atj-test-value-to-type (atj-test-value-fix test-value)) (atj-test-value-to-type test-value)))
Theorem:
(defthm atj-test-value-to-type-atj-test-value-equiv-congruence-on-test-value (implies (atj-test-value-equiv test-value test-value-equiv) (equal (atj-test-value-to-type test-value) (atj-test-value-to-type test-value-equiv))) :rule-classes :congruence)