fix(LocallyNameless): change multiApp to right-recursive - #708
Merged
Conversation
lengyijun
changed the title
lengyijun
changed the title
Collaborator
|
Before I review, please fix the indentation. |
lengyijun
force-pushed
the
multiapp
branch
8 times, most recently
from
July 11, 2026 07:06
7165429 to
217635f
Compare
…ail lemma; update proofs - Redefine `multiApp` as right-recursive (`multiApp (app f a) as`) instead of left. - Switch several inductions to `List.reverseRecOn` for better compatibility with the new recursion. - Add `listFullBeta_cons_r`/`listFullBeta_cons_l`/`multiApp_tail` helpers. - Update `invert_abs_multiApp_st`, `sn_abs_app_multiApp`, `multiApp_lc`, reduction congruences, etc. - Minor tactic adjustment in `Stlc/StrongNorm`. Fixes leanprover#706
Collaborator
|
@lengyijun Can you please let me know when you are ready for this to be reviewed? In general it is a bit unpleasant to open a PR and immediate force push nearly a dozen times (I get an email every time...). I would appreciate your being a bit more intentional in this regard. |
Contributor
Author
|
Ready to review now |
chenson2018
requested changes
Jul 11, 2026
….lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
…p.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
…p.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
…p.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
…p.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
…p.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
…orm.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
…orm.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
chenson2018
reviewed
Jul 11, 2026
Collaborator
|
@lengyijun Can I ask if it is intentional that you have turned off the feature allowing maintainers to edit pull requests? This is completely your prerogative, but it does make it take longer to fix little typos like the above. I'd normally have just pushed it myself and merged at this point. |
…p.lean Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Contributor
Author
|
I am not familiar with this configuration. |
Collaborator
|
Hmm, maybe so. Usually there is a checkbox for "Allow edits by maintainers" that is selected by default. Maybe look for this next time you open a PR. |
chenson2018
approved these changes
Jul 11, 2026
chenson2018
left a comment
chenson2018
left a comment
Collaborator
There was a problem hiding this comment.
Thanks for finding and fixing this so quickly!
intgrah
pushed a commit
to intgrah/cslib
that referenced
this pull request
Jul 14, 2026
) - Redefine `multiApp` as right-recursive (`multiApp (app f a) as`) instead of left. - Switch several inductions to `List.reverseRecOn` for compatibility with the new recursion. - Add `listFullBeta_cons_r`/`listFullBeta_cons_l`/`multiApp_tail` helpers. - Update related proofs Fixes leanprover#706 --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
benbrastmckie
added a commit
to benbrastmckie/cslib
that referenced
this pull request
Jul 18, 2026
Verified against upstream: all three user PRs (leanprover#648/leanprover#662/leanprover#649) are already rebased onto latest upstream/main (056cf93, leanprover#708), 0 behind, and CI-green. leanprover#485's HML fix is redundant with fmontesi's live leanprover#607 commit 77ce0c7. Session: sess_1783880050_660057
fmontesi
pushed a commit
that referenced
this pull request
Jul 22, 2026
- Redefine `multiApp` as right-recursive (`multiApp (app f a) as`) instead of left. - Switch several inductions to `List.reverseRecOn` for compatibility with the new recursion. - Add `listFullBeta_cons_r`/`listFullBeta_cons_l`/`multiApp_tail` helpers. - Update related proofs Fixes #706 --------- Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
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.
multiAppas right-recursive (multiApp (app f a) as) instead of left.List.reverseRecOnfor compatibility with the new recursion.listFullBeta_cons_r/listFullBeta_cons_l/multiApp_tailhelpers.Fixes #706