    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Instances for rational numbers
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Rational.Instances where

    open import Data.Rational.Properties using (_≟_; ≤-isDecTotalOrder)
    open import Relation.Binary.PropositionalEquality.Properties
      using (isDecEquivalence)

    instance
      ℚ-≡-isDecEquivalence = isDecEquivalence _≟_
      ℚ-≤-isDecTotalOrder = ≤-isDecTotalOrder