		Search-engine friendly clone of the ACL2 documentation.

Stv-compile

Safe-pairlis-onto-acc

Just pairlis$ onto an accumulator, but for safety cause an error if the lists to pair up aren't the same length.

Signature
(safe-pairlis-onto-acc x y acc) → *

Definitions and Theorems

Function: safe-pairlis-onto-acc

(defun safe-pairlis-onto-acc (x y acc)
 (declare (xargs :guard t))
 (let ((__function__ 'safe-pairlis-onto-acc))
  (declare (ignorable __function__))
  (mbe
   :logic (revappend (pairlis$ x y) acc)
   :exec
   (b* (((when (and (atom x) (atom y))) acc)
        ((when (atom x))
         (raise "Too many values!")
         acc)
        ((when (atom y))
         (raise "Not enough values!")
         (safe-pairlis-onto-acc (cdr x)
                                nil (cons (cons (car x) nil) acc))))
     (safe-pairlis-onto-acc (cdr x)
                            (cdr y)
                            (cons (cons (car x) (car y)) acc))))))