1457def sha256DigestFromHex : (pi unrestricted input : Bytes . (family SHA256Result)) =
1458 (lambda unrestricted input : Bytes .
1459 (nat-eliminate
1460 (lambda unrestricted validLength : Nat . (family SHA256Result))
1461 (constructor
1462 SHA256Result
1463 SHA256Failed
1464 (constructor SHA256ErrorCode SHA256DigestLengthInvalid))
1465 (lambda unrestricted predecessor : Nat .
1466 (lambda unrestricted induction : (family SHA256Result) .
1467 (eliminate
1468 StdResult
1469 (lambda unrestricted current : (family StdResult (family SHA256ErrorCode) Bytes) .
1470 (family SHA256Result))
1471 (sha256DigestDecodeHexPairs (byte-to-nat (byte 32)) input)
1472 (branch StdFailure error . (constructor SHA256Result SHA256Failed error))
1473 (branch StdSuccess decoded . (sha256DigestFromBytes decoded)))))
1474 (naturalEqual (bytes-length input) (byte-to-nat (byte 64)))))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.