Skip to content

madman-bob/idris2-json-schema

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

30 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Idris2-JSON-Schema

Generate Idris 2 data types from a JSON Schema.

Build

Run:

make all

Generate Idris 2 types

Run:

./build/exec/json-schema schemaFile.json

to generate schemaFile.idr.

Example

Suppose we have a JSON schema filmSchema.json, given by:

{
  "type": "object",
  "properties": {
    "title": {
      "type": "string"
    },
    "year": {
      "type": "number"
    }
  }
}

Then when we run ./build/exec/json-schema filmSchema.json, we generate the filmSchema.idr file, with contents:

public export
record Main where
    constructor MkMain
    title : String
    year : Double

About

Generate Idris 2 data types from a JSON Schema

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published