		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-autoins-aux

Signature
(svtv-autoins-aux x map) → *
Arguments: x — Guard (svar-boolmasks-p x).; map — Guard (svtv-inputmap-p map).

Definitions and Theorems

Function: svtv-autoins-aux

(defun svtv-autoins-aux (x map)
  (declare (xargs :guard (and (svar-boolmasks-p x)
                              (svtv-inputmap-p map))))
  (let ((__function__ 'svtv-autoins-aux))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         ((unless (mbt (consp (car x))))
          (svtv-autoins-aux (cdr x) map))
         (var (caar x))
         ((when (eq (cdr (hons-get var (svtv-inputmap-fix map)))
                    :override-test))
          (svtv-autoins-aux (cdr x) map)))
      (cons (cons 'cons
                  (cons (cons 'quote (cons var 'nil))
                        (cons var 'nil)))
            (svtv-autoins-aux (cdr x) map)))))