------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic products of binary relations
--
-- This module is DEPRECATED. Please use
-- Data.Product.Relation.Lex.Strict directly.
------------------------------------------------------------------------

-- The definition of lexicographic product used here is suitable if
-- the left-hand relation is a strict partial order.

module Relation.Binary.Product.StrictLex where

open import Data.Product.Relation.Lex.Strict public