AlphaGitHub
Source/Packages

Std.Byte

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

114 lines19 declarations3.9 KiBSHA-256 e23a60e7bc40
Download exact fileView at revisionf5034773ad4bb52133

def · lines 78–86

byteShiftLeftTruncated

Full file
78def byteShiftLeftTruncated =
79  (lambda unrestricted value : Byte .
80    (lambda unrestricted amount : Nat .
81      (nat-eliminate
82        (lambda unrestricted current : Nat . Byte)
83        (byte 0)
84        (lambda unrestricted predecessor : Nat .
85          (lambda unrestricted induction : Byte . (byte-shift-left value (nat-to-byte amount))))
86        (nat-less-than amount byteNaturalEight))))

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.