		Search-engine friendly clone of the ACL2 documentation.

Atj-java-syntax-operations

Merge-jfields

Signature
(merge-jfields fields1 fields2) → merged-fields
Arguments: fields1 — Guard (jfield-listp fields1).; fields2 — Guard (jfield-listp fields2).
Returns: merged-fields — Type (jfield-listp merged-fields), given the guard.

Definitions and Theorems

Function: merge-jfields

(defun merge-jfields (fields1 fields2)
  (declare (xargs :guard (and (jfield-listp fields1)
                              (jfield-listp fields2))))
  (let ((__function__ 'merge-jfields))
    (declare (ignorable __function__))
    (cond ((endp fields1) fields2)
          ((endp fields2) fields1)
          (t (if (string<= (jfield->name (car fields1))
                           (jfield->name (car fields2)))
                 (cons (car fields1)
                       (merge-jfields (cdr fields1) fields2))
               (cons (car fields2)
                     (merge-jfields fields1 (cdr fields2))))))))

Theorem: jfield-listp-of-merge-jfields

(defthm jfield-listp-of-merge-jfields
  (implies (and (jfield-listp fields1)
                (jfield-listp fields2))
           (b* ((merged-fields (merge-jfields fields1 fields2)))
             (jfield-listp merged-fields)))
  :rule-classes :rewrite)