------------------------------------------------------------------------ -- The Agda standard library -- -- Lexicographic products of binary relations -- -- This module is DEPRECATED. Please use -- Data.Product.Relation.Lex.NonStrict directly. ------------------------------------------------------------------------ -- The definition of lexicographic product used here is suitable if -- the left-hand relation is a (non-strict) partial order. module Relation.Binary.Product.NonStrictLex where open import Data.Product.Relation.Lex.NonStrict public