		Search-engine friendly clone of the ACL2 documentation.

Sneaky

Sneaky-load-list

Load a list of values that were previously saved into the sneaky store.

Signature
(sneaky-load-list keys state) → (mv values state)
Returns: values — Type (true-listp values).

See sneaky-load; this just loads a list of values instead of a single value.

Definitions and Theorems

Function: sneaky-load-list

(defun sneaky-load-list (keys state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard t))
       (let ((__function__ 'sneaky-load-list))
            (declare (ignorable __function__))
            (b* (((when (atom keys)) (mv nil state))
                 ((mv first state)
                  (sneaky-load (car keys) state))
                 ((mv rest state)
                  (sneaky-load-list (cdr keys) state)))
                (mv (cons first rest) state))))

Theorem: true-listp-of-sneaky-load-list.values

(defthm true-listp-of-sneaky-load-list.values
        (b* (((mv common-lisp::?values ?state)
              (sneaky-load-list keys state)))
            (true-listp values))
        :rule-classes :type-prescription)