JSON.Simple.ToJSON

Interface and utilities for encoding Idris2 values to JSON
via an entermediate `Value` representation.

For regular algebraic data types, implementations can automatically
be derived using elaborator reflection (see module `Derive.ToJSON`)

Operators and functionality strongly influenced by Haskell's aeson
library

Definitions

interface ToJSON : Type -> Type

  Interface for encoding an Idris value as a JSON value.

Parameters: a
Constructor: 

MkToJSON

Methods:

toJSON : a -> JSON

Implementations:

ToJSON JSON

ToJSON Void

ToJSON String

ToJSON Char

ToJSON Double

ToJSON Bits8

ToJSON Bits16

ToJSON Bits32

ToJSON Bits64

ToJSON Int8

ToJSON Int16

ToJSON Int32

ToJSON Int64

ToJSON Int

ToJSON Integer

ToJSON Nat

ToJSON Bool

ToJSON a => ToJSON (Maybe a)

ToJSON a => ToJSON (List a)

ToJSON a => ToJSON (SnocList a)

ToJSON a => ToJSON (List1 a)

ToJSON a => ToJSON (Vect n a)

ToJSON ()

ToJSON a => ToJSON b => ToJSON (Either a b)

ToJSON a => ToJSON b => ToJSON (a, b)

All (ToJSON . f) ts => ToJSON (All f ts)

ToJSONKey k => ToJSON v => ToJSON (SortedMap k v)

All (ToJSON . f) ts => ToJSON (All f ts)

toJSON : ToJSON a => a -> JSON

Visibility: public export

interface ToJSONKey : Type -> Type

  Interface for encoding an Idris value as a key in a JSON object

Parameters: a
Constructor: 

MkToJSONKey

Methods:

toKey : a -> String

Implementations:

ToJSONKey String

ToJSONKey Char

ToJSONKey Double

ToJSONKey Bits8

ToJSONKey Bits16

ToJSONKey Bits32

ToJSONKey Bits64

ToJSONKey Int8

ToJSONKey Int16

ToJSONKey Int32

ToJSONKey Int64

ToJSONKey Int

ToJSONKey Integer

ToJSONKey Nat

ToJSONKey Bool

toKey : ToJSONKey a => a -> String

Visibility: public export

jpair : ToJSONKey k => ToJSON a => k -> a -> (String, JSON)

Visibility: export

encode : ToJSON a => a -> String

Visibility: export

singleField : String -> JSON -> JSON

  Encodes a value as a single-field object. The field has the given
  name.
  
  This corresponds to the `ObjectWithSingleField` option
  for encoding sum types.

Visibility: export

twoElemArray : String -> JSON -> JSON

  Encodes a value plus a string as a two-element array.
  
  This corresponds to the `TwoElemArray` option
  for encoding sum types.

Visibility: export

taggedObject : String -> String -> String -> JSON -> JSON

  Encodes a value plus a string as a tagged object.
  
  This corresponds to the `TaggedObject` option
  for encoding sum types.

Visibility: export

zipAllWith : ((x `p`) -> q x -> r x) -> All p xs -> All q xs -> All r xs

Visibility: export