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

Eq 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

lookup : String -> JSON -> Maybe JSON

Totality: total
Visibility: public export

update : (Maybe JSON -> Maybe JSON) -> String -> JSON -> JSON

Totality: total
Visibility: public export

traverseJSON : Monad m => (JSON -> m JSON) -> JSON -> m JSON

Totality: total
Visibility: public export

traverseJSON_ : Monad m => (JSON -> m ()) -> JSON -> m ()

Totality: total
Visibility: public export