Documentation
Batteries
.
Lean
.
Json
Search
return to top
source
Imports
Init
Batteries.Data.Float.Basic
Lean.Data.Json.FromToJson.Basic
Imported by
instToJsonFloat_batteries
source
@[instance_reducible]
instance
instToJsonFloat_batteries
:
Lean.ToJson
Float
Equations
One or more equations did not get rendered due to their size.