		Search-engine friendly clone of the ACL2 documentation.

Atj-pre-translation-var-reuse

Atj-mark-formals+body

Mark all the variables in the formal parameters and body of an ACL2 function definition as `new' or `old'

Signature
(atj-mark-formals+body formals body) → (mv new-formals new-body)
Arguments: formals — Guard (symbol-listp formals).; body — Guard (pseudo-termp body).
Returns: new-formals — Type (symbol-listp new-formals).; new-body — Type (pseudo-termp new-body), given the guard.

This is the top level of the marking algorithm; this top level is discussed in atj-mark-term.

Definitions and Theorems

Function: atj-mark-formals+body

(defun atj-mark-formals+body (formals body)
  (declare (xargs :guard (and (symbol-listp formals)
                              (pseudo-termp body))))
  (let ((__function__ 'atj-mark-formals+body))
    (declare (ignorable __function__))
    (b* ((marked-formals (atj-mark-vars-new formals))
         ((mv marked-body &)
          (atj-mark-term body formals nil formals)))
      (mv marked-formals marked-body))))

Theorem: symbol-listp-of-atj-mark-formals+body.new-formals

(defthm symbol-listp-of-atj-mark-formals+body.new-formals
  (b* (((mv ?new-formals ?new-body)
        (atj-mark-formals+body formals body)))
    (symbol-listp new-formals))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atj-mark-formals+body.new-body

(defthm pseudo-termp-of-atj-mark-formals+body.new-body
  (implies (and (symbol-listp formals)
                (pseudo-termp body))
           (b* (((mv ?new-formals ?new-body)
                 (atj-mark-formals+body formals body)))
             (pseudo-termp new-body)))
  :rule-classes :rewrite)

Theorem: len-of-atj-mark-formals+body.new-formals

(defthm len-of-atj-mark-formals+body.new-formals
  (b* (((mv ?new-formals ?new-body)
        (atj-mark-formals+body formals body)))
    (equal (len new-formals)
           (len formals))))