Source/Packages

Data.JSONAccess

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

1,210 lines73 declarations39.2 KiBSHA-256 1e44e4cc014b

def · lines 1164–1171

jsonWord64DigitStep

Full file
1164def jsonWord64DigitStep =
1165  (lambda unrestricted accumulator : (family ModelWord64) .
1166    (lambda unrestricted digit : Byte .
1167      (let unrestricted twice = (modelWord64ShiftLeftOne accumulator) in
1168        (let unrestricted eight = (modelWord64ShiftLeftOne (modelWord64ShiftLeftOne twice)) in
1169          (modelWord64Add (modelWord64Add eight twice)
1170            (modelWord64FromNaturalTruncated
1171              (naturalSaturatingSubtract (byte-to-nat digit) 48)))))))

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.