Basics for the Rational Numbers #
- mk' :: (
- num : Int
The numerator of the rational number is an integer.
- den : Nat
The denominator of the rational number is a natural number.
- den_nz : s.den ≠ 0
The denominator is nonzero.
- reduced : Nat.Coprime (Int.natAbs s.num) s.den
The numerator and denominator are coprime: it is in "reduced form".
- )
Rational numbers, implemented as a pair of integers num / den
such that the
denominator is positive and the numerator and denominator are coprime.
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.
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.
Instances For
Form the quotient n / d
where n d : Int
.
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.)