# Nibblep

Recognize unsigned 4-bit bytes.

- Signature
(nibblep x) → yes/no

- Returns
`yes/no` — Type (booleanp yes/no).

ACL2 has a flexible notion of `byte',
which may be signed or unsigned,
and consist of (almost) any number of bits:
see `unsigned-byte-p` and `signed-byte-p`.
But very often the unqualified term `byte'
refers to a sequence of exactly 8 bits,
represented by natural numbers below 256,
and the term `nibble' refers to half of such a byte,
i.e. a sequence of 4 bits,
represented by natural numbers below 16;
this predicate caters to this common terminology.

### Definitions and Theorems

**Function: **nibblep

(defun nibblep (x)
(declare (xargs :guard t))
(mbe :logic (unsigned-byte-p 4 x)
:exec (and (integerp x) (<= 0 x) (< x 16))))

**Theorem: **booleanp-of-nibblep

(defthm booleanp-of-nibblep
(b* ((yes/no (nibblep x)))
(booleanp yes/no))
:rule-classes :rewrite)

**Theorem: **nibblep-compound-recognizer

(defthm nibblep-compound-recognizer
(implies (nibblep x)
(and (integerp x) (<= 0 x)))
:rule-classes :compound-recognizer)

### Subtopics

- Nibble
- A fixtype of (unsigned 4-bit) nibbles.
- Nibblep-additional-theorems
- Additional theorems about
`nibble`.