AlphaGitHub
Source/Packages

Data.Bytes

packages/foundation/standard/src/Data/Bytes.alpha

1,462 lines172 declarations57.0 KiBSHA-256 55edb6a9adcd
Download exact fileView at revisionf5034773ad4bb52133

def · lines 1348–1356

dataBytesHexDigit

Full file
1348def dataBytesHexDigit =
1349  (lambda unrestricted nibble : Nat .
1350    (nat-eliminate
1351      (lambda unrestricted current : Nat . Byte)
1352      (nat-to-byte (naturalAdd (byte-to-nat (byte 87)) nibble))
1353      (lambda unrestricted predecessor : Nat .
1354        (lambda unrestricted induction : Byte .
1355          (nat-to-byte (naturalAdd (byte-to-nat (byte 48)) nibble))))
1356      (naturalLess nibble dataBytesNaturalTen)))

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.