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: support for csimp theorems in toLCNF #6757

Merged
merged 1 commit into from
Jan 25, 2025
Merged

feat: support for csimp theorems in toLCNF #6757

merged 1 commit into from
Jan 25, 2025

Conversation

zwarich
Copy link
Contributor

@zwarich zwarich commented Jan 23, 2025

This PR adds support for applying crimp theorems in toLCNF.

@zwarich zwarich added the changelog-compiler Compiler, runtime, and FFI label Jan 23, 2025
@zwarich zwarich requested a review from leodemoura as a code owner January 23, 2025 16:55
@zwarich
Copy link
Contributor Author

zwarich commented Jan 23, 2025

It's not easy to test this on master at the moment (it would require inspecting the LCNF and looking for the terms that should be rewritten), but it's relevant for making it through the prelude in bootstrap.

I think it would be possible to refactor toLCNF so that there is only one call to CSimp.replaceConstants rather than two separate calls, but I don't want to make such an invasive change at this point with a limited ability to test for subtle bugs.

@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 23, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d033804190aaff1bb82d9d5f98784301c0dd0e3e --onto f35a6020704e003995d585c7baa216982134d75f. (2025-01-23 17:18:56)

@leodemoura leodemoura added this pull request to the merge queue Jan 25, 2025
Merged via the queue into leanprover:master with commit cc260dd Jan 25, 2025
17 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees
No one assigned
Labels
changelog-compiler Compiler, runtime, and FFI 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.
3 participants
@zwarich @leanprover-community-bot @leodemoura