Data.Ratio

Definitions

record Ratio : Type -> Type

  Ratio types, represented by a numerator and denominator of type `a`.
  
  Most numeric operations require an instance `Integral a` in order to
  simplify the returned ratio and reduce storage space.

Totality: total
Visibility: export
Constructor: 

MkRatio : a -> a -> Ratio a

Projections:

.denom : Ratio a -> a

  Return the denominator of the ratio in reduced form.
  This value is guaranteed to always be positive.

.dn : Ratio a -> a

.nm : Ratio a -> a

.numer : Ratio a -> a

  Return the numerator of the ratio in reduced form.

Hints:

(IntegralGCD a, Abs a) => Abs (Ratio a)

Num a => Cast a (Ratio a)

Cast a b => Cast (Ratio a) (Ratio b)

(Cast a b, Fractional b) => Cast (Ratio a) b

Eq a => Eq (Ratio a)

IntegralGCD a => Fractional (Ratio a)

(IntegralGCD a, Neg a) => Neg (Ratio a)

IntegralGCD a => Num (Ratio a)

(Ord a, Num a) => Ord (Ratio a)

Show a => Show (Ratio a)

Rational : Type

  Rational numbers, represented as a ratio between
  two arbitrary-precision integers.
  
  Rationals can be constructed using `//`.

Totality: total
Visibility: public export

numer : Ratio a -> a

  Return the numerator of the ratio in reduced form.

Totality: total
Visibility: export

.numer : Ratio a -> a

  Return the numerator of the ratio in reduced form.

Totality: total
Visibility: export

denom : Ratio a -> a

  Return the denominator of the ratio in reduced form.
  This value is guaranteed to always be positive.

Totality: total
Visibility: export

.denom : Ratio a -> a

  Return the denominator of the ratio in reduced form.
  This value is guaranteed to always be positive.

Totality: total
Visibility: export

reduce : IntegralGCD a => Ratio a -> Ratio a

  Reduce a ratio by dividing both components by their common factor. Most
  operations automatically reduce the returned ratio, so explicitly calling
  this function is usually unnecessary.

Totality: total
Visibility: export

mkRatioMaybe : IntegralGCD a => a -> a -> Maybe (Ratio a)

  Construct a ratio of two values, returning `Nothing` if the denominator is
  zero.

Totality: total
Visibility: export

mkRatio : IntegralGCD a => a -> a -> Ratio a

  Create a ratio of two values.

Visibility: export

unsafeMkRatio : a -> a -> Ratio a

  Create a ratio of two values, unsafely assuming that they are coprime and
  the denominator is non-zero.
  WARNING: This function will behave erratically and may crash your program
  if these conditions are not met!

Totality: total
Visibility: export

(//) : {auto {conArg:1935} : IntegralGCD a} -> a -> (d : a) -> {auto 0 _ : So (d /= 0)} -> Ratio a

  Construct a ratio of two values.

Totality: total
Visibility: export
Fixity Declaration: infix operator, level 9

floor : Integral a => Ratio a -> a

  Round a ratio down to the nearest integer less than it.

Totality: total
Visibility: export