AlphaGitHub
Source/Packages

Data.SHA256Padding

packages/foundation/standard/src/Data/SHA256Padding.alpha

517 lines69 declarations22.0 KiBSHA-256 8c5044273786
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 206–226

sha256LengthEncodingStep

Full file
206def sha256LengthEncodingStep =
207  (lambda unrestricted state : (family SHA256LengthEncodingState) .
208    (eliminate
209      SHA256LengthEncodingState
210      (lambda unrestricted current : (family SHA256LengthEncodingState) .
211        (family SHA256LengthEncodingState))
212      state
213      (branch
214        SHA256LengthEncodingStateValue
215        remaining
216        encoded
217        count
218        .
219        (constructor
220          SHA256LengthEncodingState
221          SHA256LengthEncodingStateValue
222          (naturalDivideUnchecked remaining byteNaturalTwoHundredFiftySix)
223          (bytes-cons
224            (nat-to-byte (naturalModuloUnchecked remaining byteNaturalTwoHundredFiftySix))
225            encoded)
226          (succ count)))))

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.