Returns 0..15 for lowercase hexadecimal and 16 for every invalid byte.
1385def sha256DigestLowerHexNibble =
1386 (lambda unrestricted value : Byte .
1387 (nat-eliminate
1388 (lambda unrestricted decimal : Nat . Nat)
1389 (nat-eliminate
1390 (lambda unrestricted lower : Nat . Nat)
1391 (byte-to-nat (byte 16))
1392 (lambda unrestricted predecessor : Nat .
1393 (lambda unrestricted induction : Nat .
1394 (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 87)))))
1395 (sha256DigestHexByteInRange value (byte 97) (byte 103)))
1396 (lambda unrestricted predecessor : Nat .
1397 (lambda unrestricted induction : Nat .
1398 (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 48)))))
1399 (sha256DigestHexByteInRange value (byte 48) (byte 58))))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.