Turn a list of two expressions into the two expressions.
(atj-jexpr-list-to-2-jexprs exprs) → (mv expr1 expr2)
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-jexpr-list-to-2-jexprs (exprs) (declare (xargs :guard (jexpr-listp exprs))) (let ((__function__ 'atj-jexpr-list-to-2-jexprs)) (declare (ignorable __function__)) (if (= (len exprs) 2) (mv (jexpr-fix (first exprs)) (jexpr-fix (second exprs))) (prog2$ (raise "Internal error: ~ the list of expressions ~x0 does not have length 2." exprs) (mv (ec-call (jexpr-fix :irrelevant)) (ec-call (jexpr-fix :irrelevant)))))))
Theorem:
(defthm jexprp-of-atj-jexpr-list-to-2-jexprs.expr1 (b* (((mv ?expr1 ?expr2) (atj-jexpr-list-to-2-jexprs exprs))) (jexprp expr1)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-jexpr-list-to-2-jexprs.expr2 (b* (((mv ?expr1 ?expr2) (atj-jexpr-list-to-2-jexprs exprs))) (jexprp expr2)) :rule-classes :rewrite)