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

chore: fix canonicalizer handling over forall/lambda #6082

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

chore: fix canonicalizer handling over forall/lambda #6082

wants to merge 2 commits into from

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Nov 14, 2024

This PR changes how the canonicalizer handles forall and lambda, replacing bvars with temporary fvars. Fixes a bug reported by @hrmacbeth on zulip.

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc November 14, 2024 22:12 Inactive
@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 Nov 14, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 14, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0d7c3ac79bd9167ce7d295f51bf3779a04f7a07 --onto 1315266dd3faeaf28d1263668cb88f2f3f5e530c. (2024-11-14 22:23:15)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0d7c3ac79bd9167ce7d295f51bf3779a04f7a07 --onto 9a8543347796e52070ff7936661ae48fcebfea60. (2024-11-14 23:47:59)

@kim-em kim-em requested a review from kmill November 14, 2024 23:16
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc November 14, 2024 23:38 Inactive
@JLimperg
Copy link
Contributor

To squeeze some more performance out of this, you could copy the instantiation strategy from ForEachExpr. The instantiateRevs there effectively batch multiple instantiate1s, which should be faster.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@kmill kmill Awaiting requested review from kmill

Assignees
No one assigned
Labels
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.
4 participants
@kim-em @leanprover-community-bot @JLimperg @eric-wieser