------------------------------------------------------------------------
-- 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."
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4