------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic ordering of lists
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Relation.Binary.Lex.Core where
open import Data.Empty using (⊥)
open import Data.Unit.Base using (⊤)
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry)
open import Data.List.Base using (List; []; _∷_)
open import Function.Base using (_∘_; flip; id)
open import Level using (Level; _⊔_)
open import Relation.Nullary.Negation.Core using (¬_)
open import Relation.Binary.Core using (Rel)
open import Data.List.Relation.Binary.Pointwise.Base
using (Pointwise; []; _∷_; head; tail)
private
variable
a ℓ₁ ℓ₂ : Level
-- The lexicographic ordering itself can be either strict or non-strict,
-- depending on whether type P is inhabited.
data Lex {A : Set a} (P : Set)
(_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) :
Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂) where
base : P → Lex P _≈_ _≺_ [] []
halt : ∀ {y ys} → Lex P _≈_ _≺_ [] (y ∷ ys)
this : ∀ {x xs y ys} (x≺y : x ≺ y) → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)
next : ∀ {x xs y ys} (x≈y : x ≈ y)
(xs<ys : Lex P _≈_ _≺_ xs ys) → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)
------------------------------------------------------------------------
-- Lexicographic orderings, using a strict ordering as the base
Lex-< : {A : Set a} (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) →
Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂)
Lex-< = Lex ⊥
Lex-≤ : {A : Set a} (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) →
Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂)
Lex-≤ = Lex ⊤
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4