38def sha256BigSigma1 =
39 (lambda unrestricted value : (family ModelWord32) .
40 (sha256XorThree
41 (modelWord32RotateRight value (byte-to-nat (byte 6)))
42 (modelWord32RotateRight value (byte-to-nat (byte 11)))
43 (modelWord32RotateRight value (byte-to-nat (byte 25)))))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.