Idris2Doc : JSON.Option

JSON.Option

(source)
Definitions
data SumEncoding : 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:
  
Eq SumEncoding
  
Show SumEncoding
defaultTaggedObject : SumEncoding
  Corresponds to `TaggedObject "tag" "contents"`

  Visibility: public export
record Options : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkOptions : SumEncoding -> Bool -> Bool -> Bool -> (String -> String) -> (String -> String) -> Options

  Projections:
  
.constructorTagModifier : Options -> String -> String
  This function is used to adjust constructor names
  during encoding and decoding
  
.fieldNameModifier : Options -> String -> String
  This function is used to adjust constructor argument names
  during encoding and decoding
  
.replaceMissingKeysWithNull : Options -> Bool
  If `True`, missing keys in a JSON objects will be
  replaced with `Null` during decoding.
  
.sum : Options -> SumEncoding
  How to encode sum types
  
.unwrapRecords : Options -> Bool
  If `True`, single constructor data types will be
  encoded without a tag for the constructor name.
  
.unwrapUnary : Options -> Bool
  If `True`, the single field from a unary data constructor
  will be unwrapped.
.sum : Options -> SumEncoding
  How to encode sum types

  Visibility: public export
sum : Options -> SumEncoding
  How to encode sum types

  Visibility: public export
.unwrapUnary : Options -> Bool
  If `True`, the single field from a unary data constructor
  will be unwrapped.

  Visibility: public export
unwrapUnary : Options -> Bool
  If `True`, the single field from a unary data constructor
  will be unwrapped.

  Visibility: public export
.replaceMissingKeysWithNull : Options -> Bool
  If `True`, missing keys in a JSON objects will be
  replaced with `Null` during decoding.

  Visibility: public export
replaceMissingKeysWithNull : Options -> Bool
  If `True`, missing keys in a JSON objects will be
  replaced with `Null` during decoding.

  Visibility: public export
.unwrapRecords : Options -> Bool
  If `True`, single constructor data types will be
  encoded without a tag for the constructor name.

  Visibility: public export
unwrapRecords : Options -> Bool
  If `True`, single constructor data types will be
  encoded without a tag for the constructor name.

  Visibility: public export
.constructorTagModifier : Options -> String -> String
  This function is used to adjust constructor names
  during encoding and decoding

  Visibility: public export
constructorTagModifier : Options -> String -> String
  This function is used to adjust constructor names
  during encoding and decoding

  Visibility: public export
.fieldNameModifier : Options -> String -> String
  This function is used to adjust constructor argument names
  during encoding and decoding

  Visibility: public export
fieldNameModifier : Options -> String -> String
  This function is used to adjust constructor argument names
  during encoding and decoding

  Visibility: public export
defaultOptions : Options
  Visibility: public export
fieldName : Named a => Options -> a -> String
  Visibility: public export
fieldNamePrim : Named a => Options -> a -> TTImp
  Visibility: public export
constructorTag : Named a => Options -> a -> String
  Visibility: public export
constructorTagPrim : Named a => Options -> a -> TTImp
  Visibility: public export
data ArgInfo : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Const : ArgInfo
  
Fields : SnocList (BoundArg 2 RegularNamed) -> ArgInfo
  
Values : SnocList (BoundArg 2 Regular) -> ArgInfo
record DCon : Type
  Totality: total
  Visibility: public export
  Constructor: 
DC : Name -> TTImp -> TTImp -> TTImp -> ArgInfo -> DCon

  Projections:
  
.applied : DCon -> TTImp
  
.args : DCon -> ArgInfo
  
.bound : DCon -> TTImp
  
.name : DCon -> Name
  
.tag : DCon -> TTImp
.name : DCon -> Name
  Visibility: public export
name : DCon -> Name
  Visibility: public export
.bound : DCon -> TTImp
  Visibility: public export
bound : DCon -> TTImp
  Visibility: public export
.applied : DCon -> TTImp
  Visibility: public export
applied : DCon -> TTImp
  Visibility: public export
.tag : DCon -> TTImp
  Visibility: public export
tag : DCon -> TTImp
  Visibility: public export
.args : DCon -> ArgInfo
  Visibility: public export
args : DCon -> ArgInfo
  Visibility: public export
isConst : DCon -> Bool
  Visibility: public export
toRegular : BoundArg n RegularNamed -> BoundArg n Regular
  Visibility: public export
dcon : Options -> Con n vs -> DCon
  Visibility: export