Top

Inst-list-p

Signature
(inst-list-p xs) → *

Definitions and Theorems

Function: inst-list-p

(defun inst-list-p (xs)
 (declare (xargs :guard t))
 (let ((__function__ 'inst-list-p))
  (declare (ignorable __function__))
  (if (atom xs)
      (equal xs nil)
   (and
    (or
       (inst-p (car xs))
       (cw "~% inst-list-p: problem in: ~p0~% Appears before: ~p1~%"
           (car xs)
           (if (consp (cdr xs)) (cdr xs) nil)))
    (inst-list-p (cdr xs))))))

Subtopics

Inst-list-p-basics: Basic theorems about inst-list-p, generated by deflist.