mathlib3 documentation

core / init.meta.json

meta inductive json :

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

Instances for json

@[protected, instance]

meta def json.string_coe :

has_coe string json

@[protected, instance]

meta def json.int_coe :

has_coe ℤ json

@[protected, instance]

meta def json.float_coe :

has_coe native.float json

@[protected, instance]

meta def json.bool_coe :

has_coe bool json

@[protected, instance]

meta def json.array_coe :

has_coe (list json) json

@[protected, instance]

meta def json.inhabited :

@[protected]

meta constant json.parse :

string → option json

@[protected]

meta constant json.unparse :

json → string

meta def json.to_format :

json → format

@[protected, instance]

meta def json.has_to_format :

has_to_format json

@[protected, instance]

meta def json.has_to_string :

has_to_string json

@[protected, instance]

meta def json.has_repr :

@[protected, instance]

meta def json.decidable_eq :

decidable_eq json