		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-type-annotation

Atj-type-unannotate-vars

Remove the type annotations from a list of variables.

Signature
(atj-type-unannotate-vars vars) → unannotated-vars
Arguments: vars — Guard (symbol-listp vars).
Returns: unannotated-vars — Type (symbol-listp unannotated-vars).

The annotating types are discarded.

Definitions and Theorems

Function: atj-type-unannotate-vars

(defun atj-type-unannotate-vars (vars)
  (declare (xargs :guard (symbol-listp vars)))
  (let ((__function__ 'atj-type-unannotate-vars))
    (declare (ignorable __function__))
    (b* (((when (endp vars)) nil)
         ((mv var &)
          (atj-type-unannotate-var (car vars)))
         (vars (atj-type-unannotate-vars (cdr vars))))
      (cons var vars))))

Theorem: symbol-listp-of-atj-type-unannotate-vars

(defthm symbol-listp-of-atj-type-unannotate-vars
  (b* ((unannotated-vars (atj-type-unannotate-vars vars)))
    (symbol-listp unannotated-vars))
  :rule-classes :rewrite)

Theorem: len-of-atj-type-unannotate-vars

(defthm len-of-atj-type-unannotate-vars
  (b* ((?unannotated-vars (atj-type-unannotate-vars vars)))
    (equal (len unannotated-vars)
           (len vars))))