Load a list of values that were previously saved into the sneaky store.
(sneaky-load-list keys state) → (mv values state)
See sneaky-load; this just loads a list of values instead of a single value.
Function:
(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:
(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)