{-# OPTIONS --cubical-compatible --safe #-}
open import Equality
module Container.Tree-sort.Example
{c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where
open Derived-definitions-and-properties eq
open import Prelude using (ℕ; zero; suc; Bool; true; false)
open import Container eq
open import Container.List eq
_≤_ : ℕ → ℕ → Bool
zero ≤ _ = true
suc _ ≤ zero = false
suc m ≤ suc n = m ≤ n
open import Container.Tree-sort eq _≤_
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 ∷ [])