360def jsonConsumeLiteral =
361 (lambda unrestricted expected : Bytes .
362 (bytes-eliminate
363 (lambda unrestricted current : Bytes .
364 (pi unrestricted input : Bytes . (family JSONLiteralResult)))
365 (lambda unrestricted input : Bytes .
366 (constructor JSONLiteralResult JSONLiteralConsumed input))
367 (lambda unrestricted expectedHead : Byte .
368 (lambda unrestricted expectedTail : Bytes .
369 (lambda unrestricted induction : (pi unrestricted input : Bytes . (family JSONLiteralResult)) .
370 (lambda unrestricted input : Bytes .
371 (nat-eliminate
372 (lambda unrestricted nonEmpty : Nat . (family JSONLiteralResult))
373 (nat-eliminate
374 (lambda unrestricted equal : Nat . (family JSONLiteralResult))
375 (constructor JSONLiteralResult JSONLiteralFailed input)
376 (lambda unrestricted predecessor : Nat .
377 (lambda unrestricted equalInduction : (family JSONLiteralResult) .
378 (induction (bytes-tail input))))
379 (byte-equal expectedHead (bytes-head input)))
380 (lambda unrestricted emptyPredecessor : Nat .
381 (lambda unrestricted emptyInduction : (family JSONLiteralResult) .
382 (constructor JSONLiteralResult JSONLiteralFailed input)))
383 (naturalIsZero (bytes-length input)))))))
384 expected))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.