Type-level version of Prelude.Rational, used only as a kind.

Use % to construct one, use :% to pattern-match on it.

Pattern-match on a type-level Rational.

Note that :% doesn't check that the Rational be Reduced nor have a non-zero denominator.

When constructing Rationals, use % instead, which not only accepts more polymorphic inputs, but also returns a Reduced result with denominator known to be non-zero.

Construct a type-level Rational from a type-level Natural.

Demoted version of FromNatural.

Singleton version of FromNatural.

Construct a type-level Rational from a type-level Integer. It fails to type-check if the Integer isn't Normalized.

Demoted version of FromInteger.

Singleton version of FromInteger.

Literal Numerator of a type-level Rational. It fails to type-check if the Rational is not Reduced.

Singleton version of Num.

Literal Denominator of a type-level Rational. It fails to type-check if the Rational is not Reduced.

Singleton version of Den.

ToRational kn kd enables constructing type-level Rationals from a numerator of kind kn and a denominator of kind kd.

Singleton version of mkRational.

Like sMkRational, but never fails, thanks to a KnownRational constraint.

Like mkRational, but fails with error where mkRational would fail with Nothing.

Type-level Rationals satisfying KnownRational can be converted to SRationals using rationalSing. Moreover, KnownRational implies that the numerator is a KnownInteger, and that the denominator is a KnownNat.

A Reduced rational number is one in which the numerator and denominator have no common denominators. Reduced fails to type-check if the given type-level Rational is not reduced, otherwise it returns the given Rational, unmodified. It also fails to type-check if the Integer numerator isn't Normalized, or if the denominator is zero.

Only reduced Rationals can be reliably constrained for equality using ~. Only reduced Rationals are KnownRationals.

The type-level functions in the KindRational module always produce reduced Rationals.

Convert an implicit KnownRational to an explicit SRational.

Normalized term-level Prelude Rational representation of the type-level Rational r.

Convert an explicit SRational r value into an implicit KnownRational r constraint.

This type represents unknown type-level Rational.

Convert a term-level Prelude.Rational into an extistentialized KnownRational wrapped in SomeRational.

NB: errors if a non-Reduced Rational is given.

Singleton type for a type-level Rational r.

A explicitly bidirectional pattern synonym relating an SRational to a KnownRational constraint.

As an expression: Constructs an explicit SRational r value from an implicit KnownRational r constraint:

SRational @r :: KnownRational r => SRational r

As a pattern: Matches on an explicit SRational r value bringing an implicit KnownRational r constraint into scope:

f :: SRational r -> ..
f SRational = {- SRational r in scope -}

Return the term-level Prelude.Rational number corresponding to r.

Convert a Prelude.Rational number into an SRational n value, where n is a fresh type-level Rational.

Shows as a type-level KindRational.Rational apears literally at the type-level. Type-checks only if the type-level Rational is Reduced.

Demoted version of ShowLit.

Singleton version of ShowLit.

Shows as a type-level KindRational.Rational apears literally at the type-level. Type-checks only if the type-level Rational is Reduced.

Demoted version of ShowsLit.

Singleton version of ShowsLit.

Shows as a type-level KindRational.Rational apears literally at the type-level. Type-checks only if the type-level Rational is Reduced.

Demoted version of ShowsPrecLit.

Singleton version of ShowsPrecLit.

Inverse of showsPrecLit.

Sign of type-level Rationals, as a type-level Integer.

• Z if zero.
• P 1 if positive.
• N 1 if negative.

Singleton version of Signum.

The Signum of a Rational equals the PNum Signum of its Numerator, as well as the Numerator of its PNum Signum.

Reciprocal of the type-level Rational. Also known as multiplicative inverse.

Singleton version of Recip. Type-checks only with a non-zero r.

Like sRecip, except it fails with Nothing when r is zero, rather than requiring to satisfy this as a type-level constraint.

Quotient of the Division of the Numerator of type-level Rational a by its Denominator, using the specified Rounding r.

forall (r :: Round) (a :: Rational).
  (KnownRational a) =>
    Rem r a  ==  a - Div r a % 1

Use this to approximate a type-level Rational to an Integer.

Singleton version of Div.

Term-level version of Div.

Takes a KindRational.Rational as input, returns a Prelude Integer.

NB: errors if the Rational denominator is 0.

Remainder from Dividing the Numerator of the type-level Rational a by its Denominator, using the specified Rounding r.

forall (r :: Round) (a :: Rational).
  (KnownRational a) =>
    Rem r a  ==  a - Div r a % 1

Term-level version of Rem.

Takes a Prelude.Rational as input, returns a Prelude.Rational.

NB: errors if the Rational denominator is 0.

Singleton version of Rem.

Get both the quotient and the Remainder of the Division of the Numerator of type-level Rational a by its Denominator, using the specified Rounding r.

forall (r :: Round) (a :: Rational).
  (KnownRational a) =>
    DivRem r a  ==  '(Div r a, Rem r a)

Term-level version of DivRem.

Takes a Prelude.Rational as input, returns a pair of (quotient, reminder).

forall (r :: Round) (a :: Rational).
  (denominator a PEq 0) =>
    divRem r a  PEq  (div r a, rem r a)

NB: errors if the Rational denominator is 0.

Singleton version of DivRem.

Rounding strategy.

Whether the type-level Rational is terminating. That is, whether it can be fully represented as a finite decimal number.

Term-level version of the IsTerminating function.

NB: errors if the Rational denominator is 0.

Determine whether r is Terminating or NonTerminating at the term-level, and create the corresponding type-level proof.

This is essentially the same as (KnownRational r, IsTerminating r ~ True), except with a nicer error message when IsTerminating r ~ False.

This is essentially the same as (KnownRational r, IsTerminating r ~ False), except with a nicer error message when IsTerminating r ~ False.

Matches a SRational that is Terminating.

Matches a SRational that is NonTerminating.

Like sameRational, but if the type-level Rationals aren't equal, this additionally provides proof of LT or GT.

We either get evidence that this function was instantiated with the same type-level Rationals, or Nothing.