------------------------------------------------------------------------ -- 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