8000 fix: use the fvar subst for erased code in LCNF simp by zwarich · Pull Request #8717 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

fix: use the fvar subst for erased code in LCNF simp #8717

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 1 commit into from
Jun 11, 2025
Merged

fix: use the fvar subst for erased code in LCNF simp #8717

merged 1 commit into from
Jun 11, 2025

Conversation

zwarich
Copy link
Contributor
@zwarich zwarich commented Jun 11, 2025

This PR uses the fvar substitution mechanism to replace erased code. This isn't entirely satisfactory, since LCNF's .return doesn't support a general Arg (which has a .erased constructor), it only supports an FVarId. This is in contrast to the IR .ret, which does support a general Arg.

@zwarich zwarich requested a review from leodemoura as a code owner June 11, 2025 05:26
@zwarich zwarich added the changelog-compiler Compiler, runtime, and FFI label Jun 11, 2025
@zwarich zwarich enabled auto-merge June 11, 2025 05:26
@zwarich zwarich added this pull request to the merge queue Jun 11, 2025
@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 Jun 11, 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 d8c54fb93d23b90f551e2d42c5fef2bc549d519c --onto 8422d936cff3b609bd2a1396e82356c82c383386. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-11 05:55:20)

Merged via the queue into leanprover:master with commit a92890e Jun 11, 2025
19 checks passed
algebraic-dev pushed a commit to algebraic-dev/lean4 that referenced this pull request Jun 18, 2025
@zwarich @algebraic-dev
fix: use the fvar subst for erased code in LCNF simp (leanprover#8717)
03f26e4 
This PR uses the fvar substitution mechanism to replace erased code.
This isn't entirely satisfactory, since LCNF's `.return` doesn't support
a general `Arg` (which has a `.erased` constructor), it only supports an
`FVarId`. This is in contrast to the IR `.ret`, which does support a
general `Arg`.
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.
2 participants
@zwarich @leanprover-community-bot
0