		Search-engine friendly clone of the ACL2 documentation.

Stv-autohyps

Stv-autohyps-aux

Signature
(stv-autohyps-aux ins stv) → *
Arguments: ins — Guard (symbol-listp ins).; stv — Guard (processed-stv-p stv).

We could have used unsigned-byte-p instead, but that gets us into trouble with :expand hints when recursive definitions of unsigned-byte-p are installed, so just use explicit bounds instead.

Definitions and Theorems

Function: stv-autohyps-aux

(defun stv-autohyps-aux (ins stv)
 (declare (xargs :guard (and (symbol-listp ins)
                             (processed-stv-p stv))))
 (let ((__function__ 'stv-autohyps-aux))
  (declare (ignorable __function__))
  (if (atom ins)
      nil
   (list*
    (cons 'natp (cons (car ins) 'nil))
    (cons
         '<
         (cons (car ins)
               (cons (cons 'expt
                           (cons '2
                                 (cons (stv-in->width (car ins) stv)
                                       'nil)))
                     'nil)))
    (stv-autohyps-aux (cdr ins) stv)))))