		Search-engine friendly clone of the ACL2 documentation.

Balance

Litp-for-levels

Signature
(litp-for-levels x levels) → *

Definitions and Theorems

Function: litp-for-levels

(defun litp-for-levels (x levels)
  (declare (xargs :stobjs (levels)))
  (declare (xargs :guard t))
  (let ((__function__ 'litp-for-levels))
    (declare (ignorable __function__))
    (and (litp x)
         (lit-in-bounds x (u32-length levels)))))