fix: use more reduction when computing parent types#7764
Merged
kim-em merged 1 commit intoleanprover:masterfrom Apr 1, 2025
Merged
fix: use more reduction when computing parent types#7764kim-em merged 1 commit intoleanprover:masterfrom
kim-em merged 1 commit intoleanprover:masterfrom
Conversation
This PR adds in more normalization for the routine that computes a parent type. Some mathlib adaptations are the result of not reducing the type parameters.
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Apr 1, 2025
ghost
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Apr 1, 2025
|
Mathlib CI status (docs):
|
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Apr 3, 2025
* chore: bump to nightly-2025-03-22 * Merge master into nightly-testing * chore: adaptations for nightly-2025-03-22 * fix * Merge master into nightly-testing * protected * chore: bump to nightly-2025-03-24 * update batteries and aesop * fixes for count_cons_of_ne * fix fix to Sym.inhabitedSym' (need `default`, not the `a` that happens to be in context) * bump heartbeats in MathlibTest/observe * fix, deprecated * fix merge * Update lean-toolchain for testing leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * update batteries * fixes for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * update batteries * fixes * chore: bump to nightly-2025-03-25 * Trigger CI for leanprover/lean4#7672 * Trigger CI for leanprover/lean4#7672 * update batteries * Trigger CI for leanprover/lean4#7672 * one fix * fixes * maxheartbeats * fixes for leanprover/lean4#7672 * fixes for leanprover/lean4#7672 * fixes for leanprover/lean4#7672 * fixes for leanprover/lean4#7672 * cleanups * . * chore: bump to nightly-2025-03-26 * update aesop * Update lean-toolchain for testing leanprover/lean4#7690 * Trigger CI for leanprover/lean4#7690 * Trigger CI for leanprover/lean4#7690 * maxHeartbeats * max heartbeats * invalidate cache * another heartbeats * bump batteries * deprecation * Update lean-toolchain for testing leanprover/lean4#7692 * Delete * chore: bump to nightly-2025-03-27 * update batteries * bump batteries * many more maxHeartbeats * chore: bump leantar v0.1.15 * invalidate cache * cache flush, take 2 * feat(Cache): root hash generation counter * 1-line fix * chore: bump to nightly-2025-03-28 * update deps * remove upstreamed * remove all adaptation notes, hooray * merge lean-pr-testing-7692 * chore: bump to nightly-2025-03-29 * Update lean-toolchain for testing leanprover/lean4#7717 * fix * Trigger CI for leanprover/lean4#7717 * Trigger CI for leanprover/lean4#7717 * fixes * fixes * Trigger CI for leanprover/lean4#7717 * fixes * fixes * fixes * fixes * got through all of mathlib * missing space * fix tests * Trigger CI for leanprover/lean4#7717 * Trigger CI for leanprover/lean4#7717 * Merge master into nightly-testing * chore: bump to nightly-2025-03-30 * Update lean-toolchain for testing leanprover/lean4#7710 * Trigger CI for leanprover/lean4#7710 * Trigger CI for leanprover/lean4#7710 * Merge master into nightly-testing * Trigger CI for leanprover/lean4#7717 * chore: remove fragile tests * chore: remove fragile tests * Trigger CI for leanprover/lean4#7710 * Update lean-toolchain for testing leanprover/lean4#7736 * how did this get dropped? * Trigger CI for leanprover/lean4#7710 * Trigger CI for leanprover/lean4#7736 * deprecations in Cache * fix * chore: bump to nightly-2025-03-31 * update batteries * merge fixes * fix * fixes * Update lean-toolchain for testing leanprover/lean4#7756 * fix * Update lean-toolchain for testing leanprover/lean4#7764 * eliminate some 7717 adaptation notes * Start fixing, upstream changes needed * Trigger CI for leanprover/lean4#7756 * Fix * Fix * Fix * Fix * Trigger CI for leanprover/lean4#7756 * Trigger CI for leanprover/lean4#7756 * chore: bump to nightly-2025-04-01 * lake update * Trigger CI for leanprover/lean4#7756 * Fix * Fix * Update batteries * Fix * Fix * Trigger CI for leanprover/lean4#7756 * lake update * Fix * Fix * fix for auxlemma detection * remove mention of aux proof in Mathlib.Control.Fix * fix whatsnew * better fix * argh * unfold aux lemmas before transforming aux decls * fixes * optimization: abstract nested proofs in toadditive * docstring * revert change * fix merge * deprecations in shake * fixes * fixes * chore: bump to nightly-2025-04-02 * lake update * fixes * fix test * fix * fix merge --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
This PR adds in more normalization for the routine that computes a parent type. Some mathlib adaptations are the result of not reducing the type parameters.