------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic ordering of lists
--
-- This module is DEPRECATED. Please use Data.List.Relation.Lex.Strict
-- directly.
------------------------------------------------------------------------

-- The definition of lexicographic ordering used here is suitable if
-- the argument order is a strict partial order. The lexicographic
-- ordering itself can be either strict or non-strict, depending on
-- the value of a parameter.

module Relation.Binary.List.StrictLex where

open import Data.List.Relation.Lex.Core public
open import Data.List.Relation.Lex.Strict public
  hiding (base; halt; this; next; ²-this; ²-next)