• Top

• Sv::vl-moddb.lisp

Sv::maybe-modnamelist-p

Signature

(sv::maybe-modnamelist-p x) → *

Definitions and Theorems

Function: maybe-modnamelist-p

(defun sv::maybe-modnamelist-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'sv::maybe-modnamelist-p))
    (declare (ignorable __function__))
    (if (atom x)
        t
      (and (or (sv::modname-p (car x))
               (not (car x)))
           (sv::maybe-modnamelist-p (cdr x))))))

Theorem: maybe-modnamelist-p-of-cons

(defthm sv::maybe-modnamelist-p-of-cons
  (equal (sv::maybe-modnamelist-p (cons a b))
         (and (or (not a) (sv::modname-p a))
              (sv::maybe-modnamelist-p b))))