Basics for the Rational Numbers #
Rational numbers, implemented as a pair of integers num / den
such that the
denominator is positive and the numerator and denominator are coprime.
- mk' :: (
- num : Int
The numerator of the rational number is an integer.
- den : Nat
The denominator of the rational number is a natural number.
The denominator is nonzero.
The numerator and denominator are coprime: it is in "reduced form".
- )
Instances For
Auxiliary definition for Rat.normalize
. Constructs num / den
as a rational number,
dividing both num
and den
by g
(which is the gcd of the two) if it is not 1.
Equations
Instances For
Construct a normalized Rat
from a numerator and nonzero denominator.
This is a "smart constructor" that divides the numerator and denominator by
the gcd to ensure that the resulting rational number is normalized.
Equations
Instances For
Construct a rational number from a numerator and denominator.
This is a "smart constructor" that divides the numerator and denominator by
the gcd to ensure that the resulting rational number is normalized, and returns
zero if den
is zero.
Equations
Instances For
Implements "scientific notation" 123.4e-5
for rational numbers. (This definition is
@[irreducible]
because you don't want to unfold it. Use Rat.ofScientific_def
,
Rat.ofScientific_true_def
, or Rat.ofScientific_false_def
instead.)