		Search-engine friendly clone of the ACL2 documentation.

Svtv-to-fsm

Svtv-to-fsm-first-thm-input-var-bindings

Signature
(svtv-to-fsm-first-thm-input-var-bindings input-vars bindings overridetype envs-var) → *
Arguments: input-vars — Guard (svarlist-p input-vars).; bindings — Guard (lhprobe-map-p bindings).; overridetype — Guard (svar-overridetype-p overridetype).

Definitions and Theorems

Function: svtv-to-fsm-first-thm-input-var-bindings

(defun svtv-to-fsm-first-thm-input-var-bindings
       (input-vars bindings overridetype envs-var)
 (declare (xargs :guard (and (svarlist-p input-vars)
                             (lhprobe-map-p bindings)
                             (svar-overridetype-p overridetype))))
 (let ((__function__ 'svtv-to-fsm-first-thm-input-var-bindings))
  (declare (ignorable __function__))
  (b* (((when (atom input-vars)) nil)
       (in (car input-vars))
       (look (hons-get in bindings))
       ((unless look)
        (raise "SVTV input not found in bindings: ~x0~%"
               in)
        (svtv-to-fsm-first-thm-input-var-bindings
             (cdr input-vars)
             bindings overridetype envs-var))
       ((lhprobe probe) (cdr look)))
   (cons
    (cons
     in
     (cons
      (cons
       (if probe.signedp 'lhs-eval-signx
         'lhs-eval-zx)
       (cons
            (cons 'quote
                  (cons (lhs-change-override probe.lhs overridetype)
                        'nil))
            (cons (cons 'nth
                        (cons probe.stage (cons envs-var 'nil)))
                  'nil)))
      'nil))
    (svtv-to-fsm-first-thm-input-var-bindings
         (cdr input-vars)
         bindings overridetype envs-var)))))