gcd -is:module
base Prelude GHC.Real,
hedgehog Hedgehog.Internal.Prelude,
base-compat Prelude.Compat,
protolude Protolude Protolude.Base,
relude Relude.Numeric,
rio RIO.Prelude,
base-prelude BasePrelude,
Cabal-syntax Distribution.Compat.Prelude,
basic-prelude BasicPrelude,
ihaskell IHaskellPrelude,
clash-prelude Clash.HaskellPrelude,
ghc-lib-parser GHC.Prelude.Basic,
prelude-compat Prelude2010,
dimensional Numeric.Units.Dimensional.Prelude,
ghc-internal GHC.Internal.Real,
rebase Rebase.Prelude,
mixed-types-num Numeric.MixedTypes.PreludeHiding,
xmonad-contrib XMonad.Config.Prime,
constrained-categories Control.Category.Constrained.Prelude Control.Category.Hask,
copilot-language Copilot.Language.Prelude,
incipit-base Incipit.Base,
LambdaHack Game.LambdaHack.Core.Prelude,
cabal-install-solver Distribution.Solver.Compat.Prelude,
faktory Faktory.Prelude,
yesod-paginator Yesod.Paginator.Prelude,
distribution-opensuse OpenSuse.Prelude,
hledger-web Hledger.Web.Import gcd x y is the non-negative factor of both
x
and
y of which every common factor of
x and
y is also a factor; for example
gcd 4 2 = 2,
gcd (-4) 6 = 2,
gcd 0 4 =
4.
gcd 0 0 =
0. (That is, the common divisor
that is "greatest" in the divisibility preordering.)
Note: Since for signed fixed-width integer types,
abs
minBound < 0, the result may be negative if one of the
arguments is
minBound (and necessarily is if the other
is
0 or
minBound) for such types.
The Greatest Common Divisor is defined by:
gcd x y == gcd y x
divides z x && divides z y ==> divides z (gcd x y) (specification)
divides (gcd x y) x
Greatest common divisor. Must satisfy
\x y -> isJust (x `divide` gcd x y) && isJust (y `divide` gcd x y)
\x y z -> isJust (gcd (x * z) (y * z) `divide` z)
Greatest common divisor. Must satisfy
\x y -> isJust (x `divide` gcd x y) && isJust (y `divide` gcd x y)
\x y z -> isJust (gcd (x * z) (y * z) `divide` z)
gcd x y is the non-negative factor of both
x
and
y of which every common factor of
x and
y is also a factor; for example
gcd 4 2 = 2,
gcd (-4) 6 = 2,
gcd 0 4 =
4.
gcd 0 0 =
0. (That is, the common divisor
that is "greatest" in the divisibility preordering.)
Note: Since for signed fixed-width integer types,
abs
minBound < 0, the result may be negative if one of the
arguments is
minBound (and necessarily is if the other
is
0 or
minBound) for such types.
>>> gcd 72 60
12
Symbolic GCD as our specification. Note that we cannot really
implement the GCD function since it is not symbolically terminating.
So, we instead uninterpret and axiomatize it below.
NB. The concrete part of the definition is only used in calls to
traceExecution and is not needed for the proof. If you don't
need to call
traceExecution, you can simply ignore that part
and directly uninterpret. In that case, we simply use Prelude's
version.
It is only a monoid for non-negative numbers.
idt <*> GCD (-2) = GCD 2
Thus, use this Monoid only for non-negative numbers!
Type-level greatest common denominator (GCD).
Note that additional equations are provided by the type-checker plugin
solver
GHC.TypeLits.Extra.Solver.
Greatest common divisor for type-level naturals.
Example:
>>> :kind! Gcd 9 11
Gcd 9 11 :: Natural
= 1
>>> :kind! Gcd 9 12
Gcd 9 12 :: Natural
= 3
The greatest common divisor of two type-level integers
Compute greatest common divisor.
Number of bytes allocated since the previous GC
The amount of memory lost due to block fragmentation in bytes. Block
fragmentation is the difference between the amount of blocks retained
by the RTS and the blocks that are in use. This occurs when megablocks
are only sparsely used, eg, when data that cannot be moved retains a
megablock.
Total amount of live data in compact regions
Total amount of data copied during this GC
The CPU time used during GC itself
The time elapsed during GC itself
The generation number of this GC