(atj-select-mv-term-types indices mv-types) → selected-mv-types
Function:
(defun atj-select-mv-term-types (indices mv-types) (declare (xargs :guard (and (nat-listp indices) (atj-type-listp mv-types)))) (let ((__function__ 'atj-select-mv-term-types)) (declare (ignorable __function__)) (b* (((unless (mbt (nat-listp indices))) (repeat (len indices) (atj-type-irrelevant))) ((unless (mbt (atj-type-listp mv-types))) (repeat (len indices) (atj-type-irrelevant))) ((when (endp indices)) nil) (index (car indices)) ((unless (< index (len mv-types))) (raise "Internal error: ~ index ~x0 has no corresponding type in ~x1." index mv-types) (repeat (len indices) (atj-type-irrelevant))) (type (nth index mv-types)) (rest-types (atj-select-mv-term-types (cdr indices) mv-types))) (cons type rest-types))))
Theorem:
(defthm atj-type-listp-of-atj-select-mv-term-types (b* ((selected-mv-types (atj-select-mv-term-types indices mv-types))) (atj-type-listp selected-mv-types)) :rule-classes :rewrite)
Theorem:
(defthm len-of-atj-select-mv-term-types (b* ((?selected-mv-types (atj-select-mv-term-types indices mv-types))) (equal (len selected-mv-types) (len indices))))