Data.IntegralGCD

Definitions

interface IntegralGCD : Type -> Type

  An interface for integer types that it is possible to take the GCD
  (greatest common denominator) of.
  
  This interface exists for totality purposes: Euclid's algorithm is
  possible to implement for any type that satisfies `Integral`, but it
  is not provably total unless that implementation satisfies some properties.
  
  Implementing this interface asserts to the compiler that Euclid's algorithm
  is total on this type.

Parameters: a
Constraints: Eq a, Integral a
Methods:

gcd : a -> a -> a

Implementations:

IntegralGCD Integer

IntegralGCD Int

IntegralGCD Int8

IntegralGCD Int16

IntegralGCD Int32

IntegralGCD Int64

IntegralGCD Bits8

IntegralGCD Bits16

IntegralGCD Bits32

IntegralGCD Bits64

gcd : IntegralGCD a => a -> a -> a

Totality: total
Visibility: public export