ATJ type of an ACL2 value.
(atj-type-of-value val) → type
This is the type that ATJ assigns to a quoted constant
with the given value.
Note that a constant like
Function:
(defun atj-type-of-value (val) (declare (xargs :guard t)) (let ((__function__ 'atj-type-of-value)) (declare (ignorable __function__)) (cond ((integerp val) (atj-type-acl2 (atj-atype-integer))) ((rationalp val) (atj-type-acl2 (atj-atype-rational))) ((acl2-numberp val) (atj-type-acl2 (atj-atype-number))) ((characterp val) (atj-type-acl2 (atj-atype-character))) ((stringp val) (atj-type-acl2 (atj-atype-string))) ((booleanp val) (atj-type-acl2 (atj-atype-boolean))) ((symbolp val) (atj-type-acl2 (atj-atype-symbol))) ((consp val) (atj-type-acl2 (atj-atype-cons))) (t (prog2$ (raise "Internal errror: ~ the value ~x0 is not a number, ~ a character, a string, a symbol, or a CONS." val) (atj-type-irrelevant))))))
Theorem:
(defthm atj-typep-of-atj-type-of-value (b* ((type (atj-type-of-value val))) (atj-typep type)) :rule-classes :rewrite)