Drop leading whitespace. When the first byte is not whitespace (the common
case for compact JSON, which has no inter-token whitespace) the answer is the
input unchanged, so we short-circuit in O(1) instead of running a
length-sized fold of no-ops. Only a genuine leading whitespace run pays the
O(run) fold. Behaviour is identical to `jsonDropWhitespaceWithFuel` over the
full length.
345def jsonDropWhitespace =
346 (lambda unrestricted input : Bytes .
347 (nat-eliminate
348 (lambda unrestricted nonEmpty : Nat . Bytes)
349 (nat-eliminate
350 (lambda unrestricted leadingWhitespace : Nat . Bytes)
351 input
352 (lambda unrestricted whitespacePredecessor : Nat .
353 (lambda unrestricted whitespaceInduction : Bytes .
354 (jsonDropWhitespaceWithFuel (bytes-length input) input)))
355 (jsonByteIsWhitespace (bytes-head input)))
356 (lambda unrestricted emptyPredecessor : Nat .
357 (lambda unrestricted emptyInduction : Bytes . input))
358 (naturalIsZero (bytes-length input))))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.