mathlib documentation

core.init.meta.json

meta inductive json :

Type

of_string : string → json
of_int : ℤ → json
of_float : native.float → json
of_bool : bool → json
null : json
object : list (string × json) → json
array : list json → json

@[instance]

meta def json.string_coe :

has_coe string json

@[instance]

meta def json.int_coe :

has_coe ℤ json

@[instance]

meta def json.float_coe :

has_coe native.float json

@[instance]

meta def json.bool_coe :

has_coe bool json

@[instance]

meta def json.array_coe :

has_coe (list json) json

@[instance]

meta def json.inhabited :

meta constant json.parse (a : string) :

meta constant json.unparse (a : json) :

meta def json.to_format (a : json) :

@[instance]

meta def json.has_to_format :

has_to_format json

@[instance]

meta def json.has_to_string :

has_to_string json

@[instance]

meta def json.has_repr :