Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: utilities for using scientific notation and floats in json #1464

Merged
merged 1 commit into from
Aug 16, 2022
Merged

feat: utilities for using scientific notation and floats in json #1464

merged 1 commit into from
Aug 16, 2022

Conversation

EdAyers
Copy link
Contributor

@EdAyers EdAyers commented Aug 12, 2022 •
edited by leodemoura
Loading

@leodemoura
Copy link
Member

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

@EdAyers
Copy link
Contributor Author

EdAyers commented Aug 13, 2022

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

@EdAyers EdAyers force-pushed the float-scientific branch 2 times, most recently from 0806270 to 5d80e8b Compare August 16, 2022 13:37
@EdAyers
Copy link
Contributor Author

EdAyers commented Aug 16, 2022

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

@EdAyers EdAyers marked this pull request as ready for review August 16, 2022 13:38
@leodemoura leodemoura enabled auto-merge (rebase) August 16, 2022 14:45
@leodemoura leodemoura merged commit 2e99e8c into leanprover:master Aug 16, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@EdAyers @leodemoura