    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Rational numbers
    ------------------------------------------------------------------------

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

    module Data.Rational where

    ------------------------------------------------------------------------
    -- Publicly re-export contents of core module and queries

    open import Data.Rational.Base public
    open import Data.Rational.Properties public
      using (_≟_; _≤?_; _<?_; _≥?_; _>?_)

    ------------------------------------------------------------------------
    -- Deprecated

    -- Version 1.0

    open import Data.Rational.Properties public
      using (drop-*≤*; ≃⇒≡; ≡⇒≃)

    -- Version 1.5

    import Data.Integer.Show as ℤ
    open import Data.String.Base using (String; _++_)

    show : ℚ → String
    show p = ℤ.show (↥ p) ++ "/" ++ ℤ.show (↧ p)

    {-# WARNING_ON_USAGE show
    "Warning: show was deprecated in v1.5.
    Please use Data.Rational.Show's show instead."
    #-}