		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Sd-natlist-linear-increments-p

Signature
(sd-natlist-linear-increments-p x) → *
Arguments: x — Guard (nat-listp x).

Definitions and Theorems

Function: sd-natlist-linear-increments-p

(defun sd-natlist-linear-increments-p (x)
 (declare (xargs :guard (nat-listp x)))
 "One reason we might bump the priority is if the wires are linearly
   progressing and we're missing one in the middle."
 (let ((__function__ 'sd-natlist-linear-increments-p))
   (declare (ignorable __function__))
   (cond ((atom x) t)
         ((atom (cdr x)) t)
         (t (and (equal (+ 1 (first x)) (second x))
                 (sd-natlist-linear-increments-p (cdr x)))))))