		Search-engine friendly clone of the ACL2 documentation.

Vl-make-res-occs

Vl-make-res-sexpr

Generate a ACL2::4v-res expression to resolve a list of emodwires.

(vl-make-res-sexpr args) generates a 4v-sexpr that joins together all of its arguments with ACL2::4v-res operations.

Note that the RES operation is commutative and associative, so any nest of RES operations is equivalent. So, we just resolve the arguments in a straightforward, right-associative manner.

Definitions and Theorems

Function: vl-make-res-sexpr

(defun vl-make-res-sexpr (args)
  (declare (xargs :guard (vl-emodwirelist-p args)))
  (cond ((atom args) acl2::*4vz-sexpr*)
        ((atom (cdr args)) (car args))
        (t (acl2::hons-list 'acl2::res
                            (car args)
                            (vl-make-res-sexpr (cdr args))))))

Theorem: 4v-sexpr-vars-of-vl-make-res-sexpr

(defthm 4v-sexpr-vars-of-vl-make-res-sexpr
  (implies (force (vl-emodwirelist-p args))
           (equal (acl2::4v-sexpr-vars (vl-make-res-sexpr args))
                  (mergesort args))))