instance instOfScientificJsonNumber : OfScientific Lean.JsonNumber

Equations

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

instance instNegJsonNumber : Neg Lean.JsonNumber

Equations

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

instance instToJsonFloat : Lean.ToJson Float

Equations

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