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