Documentation

Batteries.Lean.Json

source
@[implicit_reducible]
instance instOfScientificJsonNumber_batteries :
OfScientific Lean.JsonNumber
source
@[implicit_reducible]
instance instNegJsonNumber_batteries :
Neg Lean.JsonNumber
source
@[implicit_reducible]
instance instToJsonFloat_batteries :
Lean.ToJson Float