		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-easy-bindings-svtv-vars

Signature
(svtv-easy-bindings-svtv-vars x) → *
Arguments: x — Some arguments to easy-bindings.

Definitions and Theorems

Function: svtv-easy-bindings-svtv-vars

(defun svtv-easy-bindings-svtv-vars (x)
 (declare (xargs :guard t))
 (let ((__function__ 'svtv-easy-bindings-svtv-vars))
  (declare (ignorable __function__))
  (cond
   ((atom x) nil)
   ((symbolp (car x))
    (cons (car x)
          (svtv-easy-bindings-svtv-vars (cdr x))))
   ((atom (car x))
    (raise "Illegal argumen to svtv-easy-bindings: ~x0"
           (car x)))
   ((or (eq (caar x) :nat)
        (eq (caar x) :int)
        (eq (caar x) :bool)
        (eq (caar x) :skip))
    (svtv-easy-bindings-svtv-vars (cdr x)))
   ((or (eq (caar x) :mix)
        (eq (caar x) :seq))
    (let ((elems (cdar x)))
      (append (svtv-easy-bindings-svtv-vars elems)
              (svtv-easy-bindings-svtv-vars (cdr x)))))
   ((eq (caar x) :rev)
    (append (svtv-easy-bindings-svtv-vars (cdar x))
            (svtv-easy-bindings-svtv-vars (cdr x))))
   (t
    (raise
     "Arguments to svtv-easy-bindings should be input names or ~
                 a :mix, :seq, or :rev form, so ~x0 is illegal."
     (car x))))))