Closed rbarreiro closed 4 years ago
I have copied Language.JSON from idris-dev contrib, all changes were minor and just to make idris2 happy. The largest change I made was to include intToHexString in Json.Data since Bits and b16ToHexString are not yet on idris2.
Great, thanks for the port! Hopefully the Bits primitives will be here soonish.
I have copied Language.JSON from idris-dev contrib, all changes were minor and just to make idris2 happy. The largest change I made was to include intToHexString in Json.Data since Bits and b16ToHexString are not yet on idris2.