1782def jsonParseDocumentUnchecked =
1783 (lambda unrestricted input : Bytes .
1784 (eliminate
1785 UTF8DecodeResult
1786 (lambda unrestricted current : (family UTF8DecodeResult) . (family JSONDocumentResult))
1787 (decodeUTF8 input)
1788 (branch
1789 UTF8DecodeSucceeded
1790 codepoints
1791 .
1792 (eliminate
1793 JSONParseResult
1794 (lambda unrestricted current : (family JSONParseResult) . (family JSONDocumentResult))
1795 (jsonParserValue (jsonParserWithFuel (bytes-length input)) input)
1796 (branch
1797 JSONParsed
1798 value
1799 remaining
1800 .
1801 (app
1802 (lambda unrestricted trailing : Bytes .
1803 (nat-eliminate
1804 (lambda unrestricted empty : Nat . (family JSONDocumentResult))
1805 (constructor
1806 JSONDocumentResult
1807 JSONDocumentFailed
1808 (constructor JSONErrorCode JSONTrailingBytes)
1809 (naturalSaturatingSubtract (bytes-length input) (bytes-length trailing)))
1810 (lambda unrestricted predecessor : Nat .
1811 (lambda unrestricted induction : (family JSONDocumentResult) .
1812 (constructor JSONDocumentResult JSONDocumentParsed value)))
1813 (naturalIsZero (bytes-length trailing))))
1814 (jsonDropWhitespace remaining)))
1815 (branch
1816 JSONParseFailed
1817 code
1818 remaining
1819 .
1820 (constructor
1821 JSONDocumentResult
1822 JSONDocumentFailed
1823 code
1824 (naturalSaturatingSubtract (bytes-length input) (bytes-length remaining))))))
1825 (branch
1826 UTF8DecodeFailed
1827 code
1828 offset
1829 .
1830 (constructor
1831 JSONDocumentResult
1832 JSONDocumentFailed
1833 (constructor JSONErrorCode JSONInvalidUTF8)
1834 (modelWord32ToNatural offset)))))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.