Idris2Doc : JSON.Option

JSON.Option

(source)

Definitions

dataSumEncoding : Type
  Specifies how to encode constructors of a sum datatype.

Totality: total
Visibility: public export
Constructors:
UntaggedValue : SumEncoding
  Constructor names won't be encoded. Instead only the contents of the
constructor will be encoded as if the type had a single constructor. JSON
encodings have to be disjoint for decoding to work properly.

When decoding, constructors are tried in the order of definition. If some
encodings overlap, the first one defined will succeed.

Note: Nullary constructors are encoded as strings (using
constructorTagModifier). Having a nullary constructor
alongside a single field constructor that encodes to a
string leads to ambiguity.

Note: Only the last error is kept when decoding, so in the case of
malformed JSON, only an error for the last constructor will be reported.
ObjectWithSingleField : SumEncoding
  A constructor will be encoded to an object with a single field named
after the constructor tag (modified by the constructorTagModifier) which
maps to the encoded contents of the constructor.
TwoElemArray : SumEncoding
  A constructor will be encoded to a 2-element array where the first
element is the tag of the constructor (modified by the constructorTagModifier)
and the second element the encoded contents of the constructor.
TaggedObject : String->String->SumEncoding
  A constructor will be encoded to an object with a field `tagFieldName`
which specifies the constructor tag (modified by the
constructorTagModifier). If the constructor is a record the
encoded record fields will be unpacked into this object. So
make sure that your record doesn't have a field with the
same label as the tagFieldName. Otherwise the tag gets
overwritten by the encoded value of that field! If the constructor
is not a record the encoded constructor contents will be
stored under the contentsFieldName field.

Hints:
EqSumEncoding
GenericSumEncoding [[], [], [], [String, String]]
MetaSumEncoding [[], [], [], [String, String]]
ShowSumEncoding
defaultTaggedObject : SumEncoding
  Corresponds to `TaggedObject "tag" "contents"`

Visibility: public export
adjustConnames : (String->String) ->TypeInfo'kkss->TypeInfo'kkss
Visibility: public export
adjustInfo : (String->String) -> (String->String) ->TypeInfo'kkss->TypeInfo'kkss
Visibility: public export
adjustFieldNames : (String->String) ->TypeInfo'kkss->TypeInfo'kkss
Visibility: public export
nullaryInjections : NP_ (Listk) (ConInfo_k) kss-> (0_ : EnumTypekss) ->NP_ (Listk) (K (NS_ (Listk) (NPf) kss)) kss
Visibility: public export