888def sha256NaturalToWord64 =
889 (lambda unrestricted value : Nat .
890 (eliminate
891 SHA256LengthEncodingResult
892 (lambda unrestricted current : (family SHA256LengthEncodingResult) .
893 (family SHA256NaturalWord64Result))
894 (sha256EncodeBitLength value)
895 (branch
896 SHA256LengthEncodingSucceeded
897 encoded
898 encodedValue
899 .
900 (eliminate
901 DataBytesWord64DecodeResult
902 (lambda unrestricted current : (family DataBytesWord64DecodeResult) .
903 (family SHA256NaturalWord64Result))
904 (dataBytesReadWord64BE encoded)
905 (branch
906 DataBytesWord64Decoded
907 word
908 remaining
909 .
910 (nat-eliminate
911 (lambda unrestricted empty : Nat . (family SHA256NaturalWord64Result))
912 (constructor
913 SHA256NaturalWord64Result
914 SHA256NaturalWord64Failed
915 (constructor SHA256ErrorCode SHA256LengthEncodingInvalid))
916 (lambda unrestricted predecessor : Nat .
917 (lambda unrestricted induction : (family SHA256NaturalWord64Result) .
918 (constructor SHA256NaturalWord64Result SHA256NaturalWord64Succeeded word)))
919 (naturalIsZero (bytes-length remaining))))
920 (branch
921 DataBytesWord64DecodeFailed
922 decodeError
923 .
924 (constructor
925 SHA256NaturalWord64Result
926 SHA256NaturalWord64Failed
927 (constructor SHA256ErrorCode SHA256LengthEncodingInvalid)))))
928 (branch
929 SHA256LengthEncodingFailed
930 error
931 remaining
932 .
933 (constructor SHA256NaturalWord64Result SHA256NaturalWord64Failed error))))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.