		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-autobinds-aux

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

Definitions and Theorems

Function: svtv-autobinds-aux

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