		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vector

Svtv-flex-bindings

Generating G-bindings from an SVTV using gl::flex-bindings.

Signature
(svtv-flex-bindings svtv order &key arrange) → *
Arguments: svtv — The SVTV you are dealing with.
Guard (svtv-p svtv).; order — The variable order you want to use.; arrange — Arrangement of the indices.

Definitions and Theorems

Function: svtv-flex-bindings-fn

(defun svtv-flex-bindings-fn (svtv order arrange)
 (declare (xargs :guard (svtv-p svtv)))
 (let ((__function__ 'svtv-flex-bindings))
   (declare (ignorable __function__))
   (b*
    ((binds (svtv-easy-bindings-main order svtv))
     (arrange1 (or arrange
                   (gl::auto-bindings-list-collect-arrange
                        (gl::auto-bind-xlate-list binds nil))))
     (unbound
          (set-difference-equal (svtv->ins svtv)
                                (strip-cars (strip-cdrs arrange1))))
     (unbound-binds (svtv-easy-bindings-main unbound svtv))
     (unbound-arrange
          (gl::auto-bindings-list-collect-arrange
               (gl::auto-bind-xlate-list unbound-binds nil))))
    (gl::flex-bindings-fn (append binds unbound-binds)
                          (append arrange1 unbound-arrange)
                          0))))