Idris2Doc : Language.JSON.Data

Language.JSON.Data

Definitions

data JSON : Type
Totality: total
Visibility: public export
Constructors:
JNull : JSON
JBoolean : Bool -> JSON
JNumber : Double -> JSON
JString : String -> JSON
JArray : List JSON -> JSON
JObject : List (String, JSON) -> JSON

Hints:
Cast () JSON
Cast Bool JSON
Cast Double JSON
Cast String JSON
Cast a JSON => Cast (List a) JSON
Show JSON
format : {default 0 _ : Nat} -> Nat -> JSON -> String
  Format a JSON value, indenting by `n` spaces per nesting level.

@curr The current indentation amount, measured in spaces.
@n The amount of spaces to indent per nesting level.

Totality: total
Visibility: export