FGL binder that checks whether X is syntactically a signed integer of length at most
(check-signed-byte-p ans n x) → *
See fgl-syntactic-checker-binders and see binder for details.
Function:
(defun check-signed-byte-p (ans n x) (declare (xargs :guard t)) (let ((__function__ 'check-signed-byte-p)) (declare (ignorable __function__)) (and (signed-byte-p n x) ans t)))
Theorem:
(defthm check-signed-byte-p-implies-signed-byte-p (implies (acl2::rewriting-negative-literal (cons 'check-signed-byte-p (cons ans (cons n (cons x 'nil))))) (iff (check-signed-byte-p ans n x) (and (signed-byte-p n x) (hide (check-signed-byte-p ans n x))))))