------------------------------------------------------------------------ -- The Agda standard library -- -- An implementation of insertion sort and its properties ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Bundles using (DecTotalOrder) module Data.List.Sort.InsertionSort {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where open import Data.List.Sort.InsertionSort.Base O public open import Data.List.Sort.InsertionSort.Properties O using (insertionSort) public