------------------------------------------------------------------------ -- The Agda standard library -- -- An implementation of merge sort along with proofs of correctness. ------------------------------------------------------------------------ -- Unless you are need a particular property of MergeSort, you should -- import and use the sorting algorithm from `Data.List.Sort` instead -- of this file. {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Bundles using (DecTotalOrder) module Data.List.Sort.MergeSort {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where open import Data.List.Sort.MergeSort.Base O public open import Data.List.Sort.MergeSort.Properties O using (mergeSort) public