Skip to content

JSON related fixes. - #35

Open
ilya-fiveisky wants to merge 1 commit into
gallais:masterfrom
ilya-fiveisky:json-fixes
Open

ilya-fiveisky wants to merge 1 commit into
gallais:masterfrom
ilya-fiveisky:json-fixes

Conversation

@ilya-fiveisky

Copy link
Copy Markdown

Motivated by the fact that examples/JSONTest.agda didn't type-check, JSON related stuff was modified in a way similar to other formats in examples, i.e.:

  1. Text.Parser.JSON now uses Parser from Text.Parser instead of one from Text.Parser.Types.
  2. JSONTest.agda from examples was renamed to JSONIO.agda (because, honestly, it's more IO usage example than JSON parser usage) with corresponding fixes in the code.
  3. Added JSON.agda to examples with runParser usage example. I didn't use ∈ here (as in other examples) because runParser usage is what potential user would like to see in examples instead of diving into ∈ definition in order to see how it really parses a string.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant