		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-autohyps-aux

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

Definitions and Theorems

Function: svtv-autohyps-aux

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