------------------------------------------------------------------------
-- 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."
#-}