		Search-engine friendly clone of the ACL2 documentation.

Logops-byte-functions

Bsp-size

(bsp-size (bsp size pos)) = size

Signature
(bsp-size bsp) → size
Arguments: bsp — Guard (bspp bsp).
Returns: size — Type (and (integerp size) (>= size 0)), given (bspp bsp).

This is analogous to Common Lisp's (byte-size bytespec).

Definitions and Theorems

Function: bsp-size

(defun bsp-size (bsp)
  (declare (xargs :guard (bspp bsp)))
  (let ((__function__ 'bsp-size))
    (declare (ignorable __function__))
    (car bsp)))

Theorem: bsp-size-type

(defthm bsp-size-type
  (implies (bspp bsp)
           (b* ((size (bsp-size bsp)))
             (and (integerp size) (>= size 0))))
  :rule-classes :type-prescription)