draft #9843
Closed
draft #9843
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…hlib4 into nightly-testing # Please enter a commit message to explain why this merge is necessary, # especially if it merges an updated upstream into a topic branch. # # Lines starting with '#' will be ignored, and an empty message aborts # the commit.
(cherry picked from commit 68908a1)
…hlib4 into nightly-testing
github-merge-queue bot
pushed a commit
to leanprover/lean4
that referenced
this pull request
Feb 1, 2024
…s in structure instance elaboration (#2478) Modifies the structure instance elaborator to 1. Fill in missing fields from sources in strict left-to-right order. In `{a, b with}`, sometimes the elaborator would ignore `a` even if both `a` and `b` provided the same field, depending on what subobject fields they had. 2. Use the sources, or subobjects of the sources, to fill in entire subobjects of the target structure as much as possible. Currently, a field cannot be filled directly by a source itself resulting in the term being eta expanded. This change avoids this unnecessary and surprisingly costly extra eta expansion. Adds two new tests to illustrate the performance benefit (one courtesy @semorrison). These are currently failing on master and succeed on this branch. There is one additional test to exercise the changes to the elaboration of structure instances. Changes to make mathlib build are in leanprover-community/mathlib4#9843 Closes #2451
leanprover-community-mathlib4-bot
added
the
merge-conflict
kim-em
added a commit
that referenced
this pull request
Feb 2, 2024
This is the adaptation PR for nightly-2024-02-01. It rolls in the branches * #9843, prepared by @mattrobball, which has the adaptations for leanprover/lean4#2478 * #10133, prepared by @semorrison, which has the adaptations for leanprover/lean4#3210 As these both landed in the same nightly, we're having to do the update in one go. Note this nightly is intended to become `v4.6.0-rc1` tomorrow. --- <!-- The text above the `---` will become the commit message when your PR is merged. Please leave a blank newline before the `---`, otherwise GitHub will format the text above it as a title. To indicate co-authors, include lines at the bottom of the commit message (that is, before the `---`) using the following format: Co-authored-by: Author Name <[email protected]> Any other comments you want to keep out of the PR commit should go below the `---`, and placed outside this HTML comment, or else they will be invisible to reviewers. If this PR depends on other PRs, please list them below this comment, using the following format: - [ ] depends on: #abc [optional extra text] - [ ] depends on: #xyz [optional extra text] --> [](https://gitpod.io/from-referrer/) --------- Co-authored-by: Kevin Buzzard <[email protected]> Co-authored-by: Matthew Ballard <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
](https://gitpod.io/from-referrer/){kind=link}
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.