------------------------------------------------------------------------ -- The Agda standard library -- -- Rational numbers in non-reduced form. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Rational.Unnormalised where -- Re-export basic definition, operations and queries open import Data.Rational.Unnormalised.Base public open import Data.Rational.Unnormalised.Properties public using (_≃?_; _≤?_; _<?_; _≥?_; _>?_)