Skip to content

[Lean] Add basic support for floats#1784

Merged
abentkamp merged 11 commits intomainfrom
lean-floats
Dec 1, 2025
Merged

[Lean] Add basic support for floats#1784
abentkamp merged 11 commits intomainfrom
lean-floats

Conversation

@clementblaudeau
Copy link
Copy Markdown
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
Copy Markdown
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
Copy Markdown
Contributor

@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 and others added 3 commits December 1, 2025 11:49
@abentkamp @W95Psp
chore(lean): small refactor
101ead2 
Co-authored-by: Lucas Franceschino <lucas@cryspen.com>
@abentkamp @W95Psp
chore(lean): small refactor
146215e 
Co-authored-by: Lucas Franceschino <lucas@cryspen.com>
@abentkamp
feat(lean): link issue in float error message
402b5e6
@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

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

1 more reviewer

@W95Psp W95Psp W95Psp approved these changes

Reviewers whose approvals may not affect merge requirements

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