		Search-engine friendly clone of the ACL2 documentation.

Mergesort

Mergesort-exec

The implementation of mergesort.

Definitions and Theorems

Function: mergesort-exec

(defun mergesort-exec (x)
  (declare (xargs :guard t))
  (cond ((atom x) nil)
        ((atom (cdr x))
         (mbe :logic (insert (car x) nil)
              :exec (list (car x))))
        (t (mv-let (part1 part2)
                   (halve-list x)
             (fast-union (mergesort-exec part1)
                         (mergesort-exec part2)
                         nil)))))