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