1687def jsonParseValueStep =
1688 (lambda unrestricted parser : (family JSONParser) .
1689 (lambda unrestricted input : Bytes .
1690 (app
1691 (lambda unrestricted clean : Bytes .
1692 (nat-eliminate
1693 (lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
1694 (app
1695 (lambda unrestricted head : Byte .
1696 (app
1697 (lambda unrestricted tail : Bytes .
1698 (nat-eliminate
1699 (lambda unrestricted string : Nat . (family JSONParseResult))
1700 (nat-eliminate
1701 (lambda unrestricted object : Nat . (family JSONParseResult))
1702 (jsonParseValueStepPart1 parser clean head tail)
1703 (lambda unrestricted objectPredecessor : Nat .
1704 (lambda unrestricted objectInduction : (family JSONParseResult) .
1705 (eliminate
1706 JSONParseResult
1707 (lambda unrestricted current : (family JSONParseResult) .
1708 (family JSONParseResult))
1709 (jsonParserObject parser tail)
1710 (branch
1711 JSONParsed
1712 members
1713 remaining
1714 .
1715 (constructor
1716 JSONParseResult
1717 JSONParsed
1718 (constructor JSON JSONObject members)
1719 remaining))
1720 (branch
1721 JSONParseFailed
1722 code
1723 remaining
1724 .
1725 (jsonParseFailure code remaining)))))
1726 (byte-equal head (byte 123)))
1727 (lambda unrestricted stringPredecessor : Nat .
1728 (lambda unrestricted stringInduction : (family JSONParseResult) .
1729 (eliminate
1730 JSONStringParseResult
1731 (lambda unrestricted current : (family JSONStringParseResult) .
1732 (family JSONParseResult))
1733 (jsonParseStringBody tail)
1734 (branch
1735 JSONStringParsed
1736 builder
1737 remaining
1738 .
1739 (constructor
1740 JSONParseResult
1741 JSONParsed
1742 (constructor JSON JSONString (bytes-builder-build builder))
1743 remaining))
1744 (branch
1745 JSONStringParseFailed
1746 code
1747 remaining
1748 .
1749 (jsonParseFailure code remaining)))))
1750 (byte-equal head (byte 34))))
1751 (bytes-tail clean)))
1752 (bytes-head clean))
1753 (lambda unrestricted emptyPredecessor : Nat .
1754 (lambda unrestricted emptyInduction : (family JSONParseResult) .
1755 (jsonParseFailure (constructor JSONErrorCode JSONUnexpectedEnd) clean)))
1756 (naturalIsZero (bytes-length clean))))
1757 (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.