Skip to content

[Lean] Add basic support for floats #1784

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
Merged
merged 11 commits into from
Dec 1, 2025
Merged

[Lean] Add basic support for floats #1784

merged 11 commits into from
Dec 1, 2025

Conversation

@clementblaudeau
Copy link
Contributor

@clementblaudeau clementblaudeau commented Nov 27, 2025 •
edited by abentkamp
Loading

  • Litterals
  • Types
  • Lib update
  • Arithmetic operations

Fixes #1715

@clementblaudeau clementblaudeau added backend Issue in one of the backends (i.e. F*, Coq, EC...) proof-lib Issues related the backend-specific definitions (in the proof-lib folder) lean Related to the Lean backend or library labels Nov 27, 2025
@clementblaudeau clementblaudeau added this to the Lean backend v1.0 milestone Nov 27, 2025
@clementblaudeau clementblaudeau linked an issue Nov 27, 2025 that may be closed by this pull request
[Lean] Add support for f32 and f64 Floats #1715
Closed
@abentkamp
Copy link
Contributor

abentkamp commented Nov 27, 2025 •
edited
Loading

It's unclear whether we want support for f16 and f128, which are experimental in Rust.

I'll make the backend throw an error when encountering these types.

W95Psp
W95Psp approved these changes Dec 1, 2025
View reviewed changes
Copy link
Member

@W95Psp W95Psp left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, I only have a few minor suggestions

@abentkamp abentkamp marked this pull request as ready for review December 1, 2025 13:16
@abentkamp abentkamp requested a review from a team as a code owner December 1, 2025 13:16
@abentkamp abentkamp self-requested a review December 1, 2025 13:16
@abentkamp abentkamp added this pull request to the merge queue Dec 1, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to a conflict with the base branch Dec 1, 2025
@abentkamp abentkamp enabled auto-merge December 1, 2025 14:50
@abentkamp abentkamp added this pull request to the merge queue Dec 1, 2025
Merged via the queue into main with commit 858a582 Dec 1, 2025
17 of 18 checks passed
@abentkamp abentkamp deleted the lean-floats branch December 1, 2025 15:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@W95Psp W95Psp W95Psp approved these changes

@abentkamp abentkamp Awaiting requested review from abentkamp abentkamp is a code owner automatically assigned from cryspen/hax

Assignees

@abentkamp abentkamp

Labels

backend Issue in one of the backends (i.e. F*, Coq, EC...) lean Related to the Lean backend or library proof-lib Issues related the backend-specific definitions (in the proof-lib folder)

Projects

None yet

Milestone

Lean backend v1.0

Development

Successfully merging this pull request may close these issues.

[Lean] Add support for f32 and f64 Floats

3 participants

@clementblaudeau @abentkamp @W95Psp