@[instance_reducible]

instance instOfScientificJsonNumber_batteries : OfScientific Lean.JsonNumber

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instNegJsonNumber_batteries : Neg Lean.JsonNumber

Equations

• instNegJsonNumber_batteries = { neg := fun (jn : Lean.JsonNumber) => { mantissa := -jn.mantissa, exponent := jn.exponent } }

@[instance_reducible]

instance instToJsonFloat_batteries : Lean.ToJson Float

Equations

• One or more equations did not get rendered due to their size.