lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

feat: utilities for using scientific notation and floats in json

Open EdAyers opened this issue 3 years ago • 2 comments

  • [x] waiting on https://github.com/leanprover/lean4/pull/1460 to include a JsonNumber.fromFloat

EdAyers avatar Aug 12 '22 09:08 EdAyers

@EdAyers We have merged #1460, is this one ready to be merged?

leodemoura avatar Aug 12 '22 21:08 leodemoura

not yet; got to write a Float → JsonNumber function.

EdAyers avatar Aug 13 '22 11:08 EdAyers

Ok I wrote a Float → JsonNumber function but it goes via toString : Float → String for now.

EdAyers avatar Aug 16 '22 13:08 EdAyers