Skip to content

fix: add OfNat instance for LeanOptionValue #11859

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
mhuisi merged 1 commit into from
Jan 13, 2026
Merged

fix: add OfNat instance for LeanOptionValue #11859

mhuisi merged 1 commit into from
Jan 13, 2026
+3 −0

Conversation

@eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented Jan 1, 2026 •
edited
Loading

This PR removes the need to write .ofNat for numeric options in lakefile.lean. Note that lake translate-config incorrectly assumed this was already legal in earlier revisions.

This replaces #11771.

@eric-wieser
fix: add OfNat instance for LeanOptionValue
18cab34 
This PR removes the need to write `.ofNat` for numeric options in `lakefile.lean`. Note that `lake translate-config` incorrectly assumed this was already legal in earlier revisions.
@eric-wieser
Copy link
Contributor Author

eric-wieser commented Jan 1, 2026

changelog-lake

@eric-wieser eric-wieser mentioned this pull request Jan 1, 2026
Closed
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jan 1, 2026
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 1, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b7360969edaa364ad0270af18466ca64e5cca69a --onto c0d5e8bc2c925bc2b60f18c929acf7d73ea9ecec. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-01 17:31:54)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jan 1, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase b7360969edaa364ad0270af18466ca64e5cca69a --onto 9b1b932242309e0286882fc4ef2b5e02034aa405. You can force reference manual CI using the force-manual-ci label. (2026-01-01 17:31:55)

@tydeu tydeu requested a review from mhuisi January 5, 2026 16:09
tydeu
tydeu approved these changes Jan 5, 2026
View reviewed changes
Copy link
Member

@tydeu tydeu left a comment

Choose a reason for hiding this comment

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

Thanks! LGTM! Since @mhuisi owns this code, I will delegate merging to him.

@mhuisi mhuisi added this pull request to the merge queue Jan 13, 2026
Merged via the queue into leanprover:master with commit abed967 Jan 13, 2026
18 of 19 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tydeu tydeu tydeu approved these changes

@mhuisi mhuisi Awaiting requested review from mhuisi

Assignees

No one assigned

Labels

changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@eric-wieser @leanprover-community-bot @leanprover-bot @tydeu @mhuisi