AlphaGitHub
Source/Packages

Data.SHA256Padding

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

480 lines68 declarations20.3 KiBSHA-256 aa838c76d642
Download exact fileView at revisionf5034773ad4bb52133

def · lines 205–225

sha256LengthEncodingStep

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