AlphaGitHub
Source/Packages

Data.JSON

packages/foundation/standard/src/Data/JSON.alpha

2,617 lines251 declarations113.9 KiBSHA-256 bd63da5ed186
Download exact fileView at revision426597bda5753d86c4

def · lines 1759–1780

jsonParserWithFuel

Full file
1759def jsonParserWithFuel =
1760  (lambda unrestricted fuel : Nat .
1761    (nat-eliminate
1762      (lambda unrestricted current : Nat . (family JSONParser))
1763      (constructor
1764        JSONParser
1765        JSONParserValue
1766        (lambda unrestricted input : Bytes .
1767          (jsonParseFailure (constructor JSONErrorCode JSONUnexpectedEnd) input))
1768        (lambda unrestricted input : Bytes .
1769          (jsonParseFailure (constructor JSONErrorCode JSONUnexpectedEnd) input))
1770        (lambda unrestricted input : Bytes .
1771          (jsonParseFailure (constructor JSONErrorCode JSONUnexpectedEnd) input)))
1772      (lambda unrestricted predecessor : Nat .
1773        (lambda unrestricted induction : (family JSONParser) .
1774          (constructor
1775            JSONParser
1776            JSONParserValue
1777            (jsonParseValueStep induction)
1778            (jsonParseObjectMembersStep induction)
1779            (jsonParseArrayValuesStep induction))))
1780      fuel))

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.