AlphaGitHub
Source/Packages

Data.JSON

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

2,617 lines251 declarations113.9 KiBSHA-256 bd63da5ed186
Download exact fileView at revision426597bda5753d86c4

def · lines 386–406

jsonHexNibble

Full file
386def jsonHexNibble =
387  (lambda unrestricted value : Byte .
388    (nat-eliminate
389      (lambda unrestricted decimal : Nat . Nat)
390      (nat-eliminate
391        (lambda unrestricted lower : Nat . Nat)
392        (nat-eliminate
393          (lambda unrestricted upper : Nat . Nat)
394          jsonNaturalSixteen
395          (lambda unrestricted predecessor : Nat .
396            (lambda unrestricted induction : Nat .
397              (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 55)))))
398          (jsonByteInHalfOpenRange value (byte 65) (byte 71)))
399        (lambda unrestricted predecessor : Nat .
400          (lambda unrestricted induction : Nat .
401            (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 87)))))
402        (jsonByteInHalfOpenRange value (byte 97) (byte 103)))
403      (lambda unrestricted predecessor : Nat .
404        (lambda unrestricted induction : Nat .
405          (naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 48)))))
406      (jsonByteIsDigit value)))

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.