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

Porting note: ext does not look through definitions, so we need more ext lemmas #5229

Closed
kim-em opened this issue Jun 18, 2023 · 1 comment
Closed

Porting note: ext does not look through definitions, so we need more ext lemmas #5229

kim-em opened this issue Jun 18, 2023 · 1 comment
Labels
porting-notes Mathlib3 to Mathlib4 porting notes.

Comments

@kim-em
Copy link
Contributor

kim-em commented Jun 18, 2023 •
edited by joneugster
Loading

Classifies porting notes claiming:

added ext lemma
added @[ext]

Links

Notes

We could either provide some automation to generate the additional ext lemmas we need now, or work out how to make ext more powerful.

See discussion on zulip: 1.
@kim-em
Copy link
Contributor Author

kim-em commented Jun 18, 2023

This link searches for references to this issue in the source code.

@joneugster joneugster added the porting-notes Mathlib3 to Mathlib4 porting notes. label Jun 18, 2024
This was referenced Jun 18, 2024
Open
Closed
@joneugster joneugster changed the title ext does not look through definitions, so we need more ext lemmas Porting note: ext does not look through definitions, so we need more ext lemmas Jun 18, 2024
@joneugster joneugster mentioned this issue Jun 18, 2024
Closed
Vierkantor added a commit that referenced this issue Oct 16, 2024
@Vierkantor
chore: classify porting notes about ext
Loading
Loading status checks…
4aa87da 
I checked all porting notes mentioning `ext` and either fixed them, or classified them as
 * #5229 if it's a new `@[ext]` lemma
 * #11041 if it's a regression in `ext`
 * #11182 if `@[ext]` had to be removed

This PR should contain only modifications to comments.
@Vierkantor Vierkantor mentioned this issue Oct 16, 2024
Closed
mathlib-bors bot pushed a commit that referenced this issue Oct 16, 2024
@Vierkantor
chore: classify porting notes about ext (#17809)
0b07d2a 
I checked all porting notes mentioning `ext` and either fixed them (see #17810), or classified them as
 * #5229 if it's a new `@[ext]` lemma
 * #11041 if it's a regression in `ext`
 * #11182 if `@[ext]` had to be removed

This PR should contain only modifications to comments.
Vierkantor added a commit that referenced this issue Oct 17, 2024
@Vierkantor
chore: remove porting notes about adding/removing @[ext] attributes
Loading
Loading status checks…
9608e6a 
All of these porting notes are about the change in behaviour of the `ext` tactic and attribute between Lean 3 and Lean 4: in Lean 4 it only accepts lemmas with conclusion `x = y` with `x` and `y` free variables, and only applies these if the types are reducibly equal. Since those behaviours are not likely to change in the future, we don't need to keep these porting notes.

I propose that we should keep #11041 since it indicates where these `ext` lemmas have not yet been added.

Closes: #5229
Closes: #11182
@Vierkantor Vierkantor mentioned this issue Oct 17, 2024
Closed
@mathlib-bors mathlib-bors bot closed this as completed in 3f297f5 Oct 17, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
porting-notes Mathlib3 to Mathlib4 porting notes.
Projects
None yet
Milestone
No milestone
2 participants
@kim-em @joneugster