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: Rat.toFloat #750

Merged
merged 3 commits into from May 13, 2024
Merged

feat: Rat.toFloat #750

merged 3 commits into from May 13, 2024

Conversation

digama0
Copy link
Member

@digama0 digama0 commented Apr 18, 2024

This adds an implementation of exact (IEEE conforming) rounding from Rat to Float rounding nearest ties to even. Note that unlike most other lean functions (but like most float functions), division by zero results in Float.inf or Float.nan, not 0.

@digama0 digama0 added the will-merge-soon PR will be merged soon. Any concerns should be raised quickly. label Apr 25, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label May 7, 2024
@semorrison semorrison merged commit 1462f41 into main May 13, 2024
3 checks passed
@semorrison semorrison deleted the rat_to_float branch May 13, 2024 01:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

Assignees
No one assigned
Labels
merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. will-merge-soon PR will be merged soon. Any concerns should be raised quickly.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@digama0 @eric-wieser @semorrison @leanprover-community-mathlib4-bot