JSON.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

Parameters: a
Constructor: 

MkToJSON

Methods:

toJSON : Encoder v => a -> v

Implementations:

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)

ToJSON a => ToJSON (SortedMap String a)

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

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

toJSON : ToJSON a => Encoder v => a -> v

Visibility: public export

jpair : ToJSON a => Encoder v => String -> a -> (String, v)

Visibility: export

=DEPRECATED=

(.=) : ToJSON a => Encoder v => String -> a -> (String, v)

  Deprecated: Use `jpair` instead

Visibility: export
Fixity Declaration: infixr operator, level 8

encodeVia : (0 v : Type) -> Encoder v => ToJSON a => a -> String

Visibility: export

encode : ToJSON a => a -> String

Visibility: export

singleField : Encoder v => String -> v -> v

  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 : Encoder v => String -> v -> v

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

Visibility: export

taggedObject : Encoder v => String -> String -> String -> v -> v

  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