------------------------------------------------------------------------
-- The Agda standard library
--
-- Sorted lists
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Relation.Binary.Bundles using (TotalOrder)
 
module Data.List.Relation.Unary.Sorted.TotalOrder
  {a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂) where
 
open TotalOrder totalOrder renaming (Carrier to A)
 
open import Data.List.Base using (List; []; _∷_)
open import Data.List.Relation.Unary.Linked as Linked using (Linked)
open import Level using (_⊔_)
open import Relation.Unary as U using (Pred; _⊆_)
open import Relation.Binary.Definitions as B
 
------------------------------------------------------------------------
-- Definition
 
Sorted : Pred (List A) (a ⊔ ℓ₂)
Sorted xs = Linked _≤_ xs
 
------------------------------------------------------------------------
-- Operations
 
module _ {x y xs} where
 
  head : Sorted (x ∷ y ∷ xs) → x ≤ y
  head = Linked.head
 
  tail : Sorted (x ∷ xs) → Sorted xs
  tail = Linked.tail
 
------------------------------------------------------------------------
-- Properties of predicates preserved by Sorted
 
sorted? : B.Decidable _≤_ → U.Decidable Sorted
sorted? = Linked.linked?
 
irrelevant : B.Irrelevant _≤_ → U.Irrelevant Sorted
irrelevant = Linked.irrelevant
 
satisfiable : U.Satisfiable Sorted
satisfiable = Linked.satisfiable