------------------------------------------------------------------------ -- The Agda standard library -- -- Compatibility module. Pending for removal. Use -- Relation.Binary.Properties.DecTotalOrder instead. ------------------------------------------------------------------------ open import Relation.Binary module Relation.Binary.Props.DecTotalOrder {d₁ d₂ d₃} (DT : DecTotalOrder d₁ d₂ d₃) where open import Relation.Binary.Properties.DecTotalOrder DT public