(sbitset-blockp x) recognizes numbers that are valid as the block component of an sbitset-pairp.
(sbitset-blockp x) → bool
To ensure that sparse bitsets are canonical, we don't allow 0 as a valid block. The idea is that any block whose value is 0 should just be omitted from the set.
(defun sbitset-blockp$inline (x) (declare (xargs :guard t)) (let ((__function__ 'sbitset-blockp)) (declare (ignorable __function__)) (mbe :logic (and (posp x) (< x (expt 2 *sbitset-block-size*))) :exec (and (integerp x) (<= 1 x) (<= x 1152921504606846975)))))
(defthm booleanp-of-sbitset-blockp (b* ((bool (sbitset-blockp$inline x))) (booleanp bool)) :rule-classes :type-prescription)
(defthm sbitset-block-type (implies (sbitset-blockp x) (posp x)) :rule-classes :compound-recognizer)
(defthm sbitset-block-upper-bound (implies (sbitset-blockp x) (< x (expt 2 *sbitset-block-size*))))