		Search-engine friendly clone of the ACL2 documentation.

Logops-byte-functions

Bsp-position

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

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

Definitions and Theorems

Function: bsp-position

(defun bsp-position (bsp)
  (declare (xargs :guard (bspp bsp)))
  (let ((__function__ 'bsp-position))
    (declare (ignorable __function__))
    (cdr bsp)))

Theorem: bsp-position-type

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