		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-var-reuse

Atj-mark-lambda-formals

Signature
(atj-mark-lambda-formals formals actuals vars-in-scope vars-used-after vars-to-mark-new) → (mv marked-formals new-vars-to-mark-new)
Arguments: formals — Guard (symbol-listp formals).; actuals — Guard (pseudo-term-listp actuals).; vars-in-scope — Guard (symbol-listp vars-in-scope).; vars-used-after — Guard (symbol-listp vars-used-after).; vars-to-mark-new — Guard (symbol-listp vars-to-mark-new).
Returns: marked-formals — Type (and (symbol-listp marked-formals) (equal (len marked-formals) (len formals))) .; new-vars-to-mark-new — Type (symbol-listp new-vars-to-mark-new), given (and (symbol-listp formals) (symbol-listp vars-to-mark-new)).

Definitions and Theorems

Function: atj-mark-lambda-formals

(defun atj-mark-lambda-formals
       (formals actuals vars-in-scope
                vars-used-after vars-to-mark-new)
 (declare (xargs :guard (and (symbol-listp formals)
                             (pseudo-term-listp actuals)
                             (symbol-listp vars-in-scope)
                             (symbol-listp vars-used-after)
                             (symbol-listp vars-to-mark-new))))
 (declare (xargs :guard (= (len formals) (len actuals))))
 (let ((__function__ 'atj-mark-lambda-formals))
  (declare (ignorable __function__))
  (b* (((when (endp formals))
        (mv nil vars-to-mark-new))
       (formal (car formals))
       (new? (or (not (member-eq formal vars-in-scope))
                 (member-eq formal vars-used-after)
                 (dumb-occur-var-open-lst formal (cdr actuals))))
       (marked-formal (if new? (atj-mark-var-new formal)
                        (atj-mark-var-old formal)))
       (vars-to-mark-new (if new? (cons formal vars-to-mark-new)
                           (remove-eq formal vars-to-mark-new)))
       ((mv marked-formals vars-to-mark-new)
        (atj-mark-lambda-formals (cdr formals)
                                 (cdr actuals)
                                 vars-in-scope
                                 vars-used-after vars-to-mark-new)))
    (mv (cons marked-formal marked-formals)
        vars-to-mark-new))))

Theorem: return-type-of-atj-mark-lambda-formals.marked-formals

(defthm return-type-of-atj-mark-lambda-formals.marked-formals
  (b* (((mv ?marked-formals ?new-vars-to-mark-new)
        (atj-mark-lambda-formals formals actuals vars-in-scope
                                 vars-used-after vars-to-mark-new)))
    (and (symbol-listp marked-formals)
         (equal (len marked-formals)
                (len formals))))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atj-mark-lambda-formals.new-vars-to-mark-new

(defthm symbol-listp-of-atj-mark-lambda-formals.new-vars-to-mark-new
 (implies
  (and (symbol-listp formals)
       (symbol-listp vars-to-mark-new))
  (b* (((mv ?marked-formals ?new-vars-to-mark-new)
        (atj-mark-lambda-formals formals actuals vars-in-scope
                                 vars-used-after vars-to-mark-new)))
    (symbol-listp new-vars-to-mark-new)))
 :rule-classes :rewrite)

Theorem: true-listp-of-atj-mark-lambda-formals.marked-formals

(defthm true-listp-of-atj-mark-lambda-formals.marked-formals
  (b* (((mv ?marked-formals ?new-vars-to-mark-new)
        (atj-mark-lambda-formals formals actuals vars-in-scope
                                 vars-used-after vars-to-mark-new)))
    (true-listp marked-formals))
  :rule-classes :type-prescription)

Theorem: true-listp-of-atj-mark-lambda-formals.new-vars-to-mark-new

(defthm true-listp-of-atj-mark-lambda-formals.new-vars-to-mark-new
 (implies
  (true-listp vars-to-mark-new)
  (b* (((mv ?marked-formals ?new-vars-to-mark-new)
        (atj-mark-lambda-formals formals actuals vars-in-scope
                                 vars-used-after vars-to-mark-new)))
    (true-listp new-vars-to-mark-new)))
 :rule-classes :type-prescription)

Theorem: len-of-atj-mark-lambda-formals.marked-formals

(defthm len-of-atj-mark-lambda-formals.marked-formals
  (b* (((mv ?marked-formals ?new-vars-to-mark-new)
        (atj-mark-lambda-formals formals actuals vars-in-scope
                                 vars-used-after vars-to-mark-new)))
    (equal (len marked-formals)
           (len formals))))