		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)))))