Get the kind (tag) of a floating-point-value structure.
(floating-point-value-kind acl2::x) → kind
Function:
(defun floating-point-value-kind$inline (acl2::x) (declare (xargs :guard (floating-point-valuep acl2::x))) (let ((__function__ 'floating-point-value-kind)) (declare (ignorable __function__)) (cond ((float-valuep acl2::x) :float) (t :double))))
Theorem:
(defthm floating-point-value-kind-possibilities (or (equal (floating-point-value-kind acl2::x) :float) (equal (floating-point-value-kind acl2::x) :double)) :rule-classes ((:forward-chaining :trigger-terms ((floating-point-value-kind acl2::x)))))