Generates a result term and a type formula for a term.
(atc-gen-uterm-result-and-type-formula uterm type affect inscope prec-tags) → (mv result type-formula type-thms)
This extends atc-gen-term-type-formula
to also return a term that is the result (in the C sense) of
Function:
(defun atc-gen-uterm-result-and-type-formula (uterm type affect inscope prec-tags) (declare (xargs :guard (and (typep type) (symbol-listp affect) (atc-symbol-varinfo-alist-listp inscope) (atc-string-taginfo-alistp prec-tags)))) (let ((__function__ 'atc-gen-uterm-result-and-type-formula)) (declare (ignorable __function__)) (b* (((mv type-formula type-thms) (atc-gen-term-type-formula uterm type affect inscope prec-tags)) ((when (type-case type :void)) (mv nil type-formula type-thms)) ((mv uterms & &) (atc-uterm-to-components uterm (1+ (len affect))))) (mv (car uterms) type-formula type-thms))))
Theorem:
(defthm symbol-listp-of-atc-gen-uterm-result-and-type-formula.type-thms (b* (((mv ?result ?type-formula ?type-thms) (atc-gen-uterm-result-and-type-formula uterm type affect inscope prec-tags))) (symbol-listp type-thms)) :rule-classes :rewrite)