1349def jsonParseObjectMembersStep =
1350 (lambda unrestricted parser : (family JSONParser) .
1351 (lambda unrestricted input : Bytes .
1352 (app
1353 (lambda unrestricted clean : Bytes .
1354 (nat-eliminate
1355 (lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
1356 (app
1357 (lambda unrestricted head : Byte .
1358 (app
1359 (lambda unrestricted tail : Bytes .
1360 (nat-eliminate
1361 (lambda unrestricted closed : Nat . (family JSONParseResult))
1362 (nat-eliminate
1363 (lambda unrestricted quote : Nat . (family JSONParseResult))
1364 (jsonParseFailure (constructor JSONErrorCode JSONObjectKeyNotString) clean)
1365 (lambda unrestricted quotePredecessor : Nat .
1366 (lambda unrestricted quoteInduction : (family JSONParseResult) .
1367 (eliminate
1368 JSONStringParseResult
1369 (lambda unrestricted current : (family JSONStringParseResult) .
1370 (family JSONParseResult))
1371 (jsonParseStringBody tail)
1372 (branch
1373 JSONStringParsed
1374 keyBuilder
1375 afterKey
1376 .
1377 (app
1378 (lambda unrestricted key : Bytes .
1379 (app
1380 (lambda unrestricted colonInput : Bytes .
1381 (nat-eliminate
1382 (lambda unrestricted nonEmpty : Nat .
1383 (family JSONParseResult))
1384 (jsonParseObjectMembersStepPart2
1385 parser
1386 key
1387 colonInput
1388 (bytes-head colonInput)
1389 (bytes-tail colonInput)
1390 (jsonParseFailure
1391 (constructor JSONErrorCode JSONObjectColonMissing)
1392 colonInput))
1393 (lambda unrestricted emptyPredecessor : Nat .
1394 (lambda unrestricted emptyInduction : (family JSONParseResult) .
1395 (jsonParseFailure
1396 (constructor JSONErrorCode JSONObjectColonMissing)
1397 colonInput)))
1398 (naturalIsZero (bytes-length colonInput))))
1399 (jsonDropWhitespace afterKey)))
1400 (bytes-builder-build keyBuilder)))
1401 (branch
1402 JSONStringParseFailed
1403 code
1404 remaining
1405 .
1406 (jsonParseFailure code remaining)))))
1407 (byte-equal head (byte 34)))
1408 (lambda unrestricted closePredecessor : Nat .
1409 (lambda unrestricted closeInduction : (family JSONParseResult) .
1410 (constructor
1411 JSONParseResult
1412 JSONParsed
1413 (constructor JSON JSONObjectEnd)
1414 tail)))
1415 (byte-equal head (byte 125))))
1416 (bytes-tail clean)))
1417 (bytes-head clean))
1418 (lambda unrestricted emptyPredecessor : Nat .
1419 (lambda unrestricted emptyInduction : (family JSONParseResult) .
1420 (jsonParseFailure (constructor JSONErrorCode JSONUnexpectedEnd) clean)))
1421 (naturalIsZero (bytes-length clean))))
1422 (jsonDropWhitespace 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.