45def sha256SmallSigma0 =
46 (lambda unrestricted value : (family ModelWord32) .
47 (sha256XorThree
48 (modelWord32RotateRight value (byte-to-nat (byte 7)))
49 (modelWord32RotateRight value (byte-to-nat (byte 18)))
50 (modelWord32ShiftRight value (byte-to-nat (byte 3)))))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.