		Search-engine friendly clone of the ACL2 documentation.

Atj-java-syntax-operations

Merge-jmethods

Signature
(merge-jmethods methods1 methods2) → merged-methods
Arguments: methods1 — Guard (jmethod-listp methods1).; methods2 — Guard (jmethod-listp methods2).
Returns: merged-methods — Type (jmethod-listp merged-methods), given the guard.

Definitions and Theorems

Function: merge-jmethods

(defun merge-jmethods (methods1 methods2)
  (declare (xargs :guard (and (jmethod-listp methods1)
                              (jmethod-listp methods2))))
  (let ((__function__ 'merge-jmethods))
    (declare (ignorable __function__))
    (cond ((endp methods1) methods2)
          ((endp methods2) methods1)
          (t (if (string<= (jmethod->name (car methods1))
                           (jmethod->name (car methods2)))
                 (cons (car methods1)
                       (merge-jmethods (cdr methods1)
                                       methods2))
               (cons (car methods2)
                     (merge-jmethods methods1 (cdr methods2))))))))

Theorem: jmethod-listp-of-merge-jmethods

(defthm jmethod-listp-of-merge-jmethods
  (implies (and (jmethod-listp methods1)
                (jmethod-listp methods2))
           (b* ((merged-methods (merge-jmethods methods1 methods2)))
             (jmethod-listp merged-methods)))
  :rule-classes :rewrite)