{-# OPTIONS --without-K #-}
module Container.Tree-sort.Example where
open import Container
open import Container.List
import Container.Tree-sort as Tree-sort
open import Equality.Propositional
open import Prelude using (ℕ; zero; suc; Bool; true; false)
_≤_ : ℕ → ℕ → Bool
zero ≤ _ = true
suc _ ≤ zero = false
suc m ≤ suc n = m ≤ n
open Tree-sort _≤_
ordered : sort (3 ∷ 1 ∷ 2 ∷ []) ≡ 1 ∷ 2 ∷ 3 ∷ []
ordered = refl
a-bag-equivalence : 1 ∷ 2 ∷ 3 ∷ [] ≈-bag 3 ∷ 1 ∷ 2 ∷ []
a-bag-equivalence = sort≈ (3 ∷ 1 ∷ 2 ∷ [])