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 102–119

sha256Word64ModuloBlockBytes

Full file
102def sha256Word64ModuloBlockBytes =
103  (lambda unrestricted value : (family ModelWord64) .
104    (eliminate
105      ModelWord64
106      (lambda unrestricted current : (family ModelWord64) . Nat)
107      value
108      (branch
109        ModelWord64Value
110        b0
111        b1
112        b2
113        b3
114        b4
115        b5
116        b6
117        b7
118        .
119        (naturalModuloUnchecked (byte-to-nat b0) sha256NaturalSixtyFour))))

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.