905def jsonIntegerFoldWithFuel =
906 (lambda unrestricted fuel : Nat .
907 (nat-eliminate
908 (lambda unrestricted current : Nat .
909 (pi unrestricted input : Bytes .
910 (pi unrestricted magnitude : Nat .
911 (pi unrestricted digits : Nat . (family JSONIntegerFoldResult)))))
912 (lambda unrestricted input : Bytes .
913 (lambda unrestricted magnitude : Nat .
914 (lambda unrestricted digits : Nat .
915 (bytes-eliminate
916 (lambda unrestricted current : Bytes . (family JSONIntegerFoldResult))
917 (constructor JSONIntegerFoldResult JSONIntegerFoldSucceeded magnitude digits)
918 (lambda unrestricted head : Byte .
919 (lambda unrestricted tail : Bytes .
920 (lambda unrestricted induction : (family JSONIntegerFoldResult) .
921 (constructor JSONIntegerFoldResult JSONIntegerFoldFailed))))
922 input))))
923 (lambda unrestricted predecessor : Nat .
924 (lambda unrestricted induction : (pi unrestricted input : Bytes . (pi unrestricted magnitude : Nat . (pi unrestricted digits : Nat . (family JSONIntegerFoldResult)))) .
925 (lambda unrestricted input : Bytes .
926 (lambda unrestricted magnitude : Nat .
927 (lambda unrestricted digits : Nat .
928 (bytes-eliminate
929 (lambda unrestricted current : Bytes . (family JSONIntegerFoldResult))
930 (constructor JSONIntegerFoldResult JSONIntegerFoldSucceeded magnitude digits)
931 (lambda unrestricted head : Byte .
932 (lambda unrestricted tail : Bytes .
933 (lambda unrestricted tailInduction : (family JSONIntegerFoldResult) .
934 (nat-eliminate
935 (lambda unrestricted digit : Nat . (family JSONIntegerFoldResult))
936 (constructor JSONIntegerFoldResult JSONIntegerFoldFailed)
937 (lambda unrestricted digitPredecessor : Nat .
938 (lambda unrestricted digitInduction : (family JSONIntegerFoldResult) .
939 (induction
940 tail
941 (naturalAdd
942 -- ten times the magnitude, folded over the TEN: a fold over
943 -- the magnitude walks its whole value (L21 finding)
944 (naturalMultiply (byte-to-nat (byte 10)) magnitude)
945 (naturalSaturatingSubtract
946 (byte-to-nat head)
947 (byte-to-nat (byte 48))))
948 (succ digits))))
949 (jsonByteIsDigit head)))))
950 input))))))
951 fuel))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.