Turn a list of two blocks into the two blocks.
(atj-jblock-list-to-2-jblocks blocks) → (mv block1 block2)
An error occurs if the list does not have length 2. This must be called when the list is expected to have length 2.
Function:
(defun atj-jblock-list-to-2-jblocks (blocks) (declare (xargs :guard (jblock-listp blocks))) (let ((__function__ 'atj-jblock-list-to-2-jblocks)) (declare (ignorable __function__)) (if (= (len blocks) 2) (mv (jblock-fix (first blocks)) (jblock-fix (second blocks))) (prog2$ (raise "Internal error: ~ the list of blocks ~x0 does not have length 2." blocks) (mv (ec-call (jblock-fix :irrelevant)) (ec-call (jblock-fix :irrelevant)))))))
Theorem:
(defthm jblockp-of-atj-jblock-list-to-2-jblocks.block1 (b* (((mv ?block1 ?block2) (atj-jblock-list-to-2-jblocks blocks))) (jblockp block1)) :rule-classes :rewrite)
Theorem:
(defthm jblockp-of-atj-jblock-list-to-2-jblocks.block2 (b* (((mv ?block1 ?block2) (atj-jblock-list-to-2-jblocks blocks))) (jblockp block2)) :rule-classes :rewrite)