		Search-engine friendly clone of the ACL2 documentation.

Utilities

Longer-than-p

(longer-than-p n x) determines if the list x is longer than n.

This can be slightly faster than (len x) when the list is long and n is small. We leave this function enabled and reason about len instead.

Definitions and Theorems

Function: longer-than-p

(defun longer-than-p (n x)
  (declare (xargs :guard (natp n)))
  (mbe :logic (< n (len x))
       :exec (cond ((zp n) (consp x))
                   ((atom x) nil)
                   (t (longer-than-p (+ -1 n) (cdr x))))))