Skip to content

fix: use _fvar._ instead of _ for anonymous fvars#12745

Merged
kim-em merged 1 commit intomasterfrom
kim/pp-fvars-anonymous-fix
Mar 1, 2026
Merged

fix: use _fvar._ instead of _ for anonymous fvars#12745
kim-em merged 1 commit intomasterfrom
kim/pp-fvars-anonymous-fix

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented Mar 1, 2026

This PR fixes pp.fvars.anonymous to display loose free variables as _fvar._ instead of _ when the option is set to false. This was the intended behavior in #12688 but the fix was committed locally and not pushed before that PR was merged.

🤖 Prepared with Claude Code

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@kim-em kim-em requested a review from kmill as a code owner March 1, 2026 09:23
@kim-em kim-em added the changelog-pp Pretty printing label Mar 1, 2026
@kim-em kim-em added this pull request to the merge queue Mar 1, 2026
@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 Mar 1, 2026
@mathlib-lean-pr-testing
Copy link

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase feea8a7611f4ec0ad13f72921f87764e4a3937bc --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-01 10:13:20)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase feea8a7611f4ec0ad13f72921f87764e4a3937bc --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-03-01 10:13:22)

Merged via the queue into master with commit ec565f3 Mar 1, 2026
29 checks passed
@github-actions
Copy link
Contributor

github-actions bot commented Mar 1, 2026

The backport to releases/v4.29.0 failed:

The process '/usr/bin/git' failed with exit code 1

To backport manually, run these commands in your terminal:

# Fetch latest updates from GitHub
git fetch
# Create a new working tree
git worktree add .worktrees/backport-releases/v4.29.0 releases/v4.29.0
# Navigate to the new working tree
cd .worktrees/backport-releases/v4.29.0
# Create a new branch
git switch --create backport-12745-to-releases/v4.29.0
# Cherry-pick the merged commit of this pull request and resolve the conflicts
git cherry-pick -x --mainline 1 ec565f3bf7a3985b6b8592f5cb5fa063b86a0ecf
# Push it to GitHub
git push --set-upstream origin backport-12745-to-releases/v4.29.0
# Go back to the original working tree
cd ../..
# Delete the working tree
git worktree remove .worktrees/backport-releases/v4.29.0

Then, create a pull request where the base branch is releases/v4.29.0 and the compare/head branch is backport-12745-to-releases/v4.29.0.

kim-em added a commit that referenced this pull request Mar 1, 2026
This PR fixes `pp.fvars.anonymous` to display loose free variables as
`_fvar._` instead of `_` when the option is set to `false`. This was the
intended behavior in #12688 but
the fix was committed locally and not pushed before that PR was merged.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

backport releases/v4.29.0 changelog-pp Pretty printing toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants