		Search-engine friendly clone of the ACL2 documentation.

Fgl-syntactic-checker-binders

Check-unsigned-byte-p

FGL binder that checks whether X is syntactically an unsigned integer of length at most n.

Signature
(check-unsigned-byte-p ans n x) → *

See fgl-syntactic-checker-binders and see binder for details.

Definitions and Theorems

Function: check-unsigned-byte-p

(defun check-unsigned-byte-p (ans n x)
  (declare (xargs :guard t))
  (let ((__function__ 'check-unsigned-byte-p))
    (declare (ignorable __function__))
    (and (unsigned-byte-p n x) ans t)))

Theorem: check-unsigned-byte-p-implies-unsigned-byte-p

(defthm check-unsigned-byte-p-implies-unsigned-byte-p
  (implies (acl2::rewriting-negative-literal
                (cons 'check-unsigned-byte-p
                      (cons ans (cons n (cons x 'nil)))))
           (iff (check-unsigned-byte-p ans n x)
                (and (unsigned-byte-p n x)
                     (hide (check-unsigned-byte-p ans n x))))))