Source/Packages

Std.Byte

packages/foundation/standard/src/Std/Byte.alpha

114 lines19 declarations3.9 KiBSHA-256 e23a60e7bc40

def · lines 43–53

byteMultiply

Full file
43def byteMultiply =
44  (lambda unrestricted left : Byte .
45    (lambda unrestricted right : Byte .
46      (app
47        (lambda unrestricted product : Nat .
48          (constructor
49            ByteMultiplyResult
50            ByteMultiplyResultValue
51            (nat-to-byte (naturalModuloUnchecked product byteNaturalTwoHundredFiftySix))
52            (nat-to-byte (naturalDivideUnchecked product byteNaturalTwoHundredFiftySix))))
53        (naturalMultiply (byte-to-nat left) (byte-to-nat right)))))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.