		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-new-to-old-thm-hints-mres

Generate the hints to prove new-to-old, when some result of a multi-value function is being transformed.

Signature
(isodata-gen-new-to-old-thm-hints-mres new-to-old-lemma-name new-to-list-of-mv-nth-name) → hints
Arguments: new-to-old-lemma-name — Guard (symbolp new-to-old-lemma-name).; new-to-list-of-mv-nth-name — Guard (symbolp new-to-list-of-mv-nth-name).
Returns: hints — A true-listp.

Definitions and Theorems

Function: isodata-gen-new-to-old-thm-hints-mres

(defun isodata-gen-new-to-old-thm-hints-mres
       (new-to-old-lemma-name new-to-list-of-mv-nth-name)
 (declare (xargs :guard (and (symbolp new-to-old-lemma-name)
                             (symbolp new-to-list-of-mv-nth-name))))
 (let ((__function__ 'isodata-gen-new-to-old-thm-hints-mres))
  (declare (ignorable __function__))
  (cons
     (cons '"Goal"
           (cons ':use
                 (cons (cons new-to-old-lemma-name
                             (cons new-to-list-of-mv-nth-name 'nil))
                       'nil)))
     'nil)))