-
Notifications
You must be signed in to change notification settings - Fork 316
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.
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
[Merged by Bors] - bug (Mathlib.Data.Finset.Sym) : suppress global variable (m : Sym alpha n) #10637
Conversation
Thanks! And you get a bonus point for removing a porting note :-) |
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by kbuzzard. |
bors r+ |
…ha n) (#10637) A global `variable {m : Sym α n}` was present in `Mathlib.Data.Finset.Sym` with the very unfortunate effect that docs#Finset.sym_eq_empty was using it : ``` theorem Finset.sym_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {n : ℕ} {m : Sym α n} : Finset.sym s n = ∅ ↔ n ≠ 0 ∧ s = ∅ ``` thus making it impossible to use to prove its goal. The line is modified, added in a few functions when needed. Co-authored-by: Antoine Chambert-Loir <[email protected]>
I assume leanprover/lean4#2452 would help here? |
I suspect the problem comes from there, but I didn't try to understand what happened. |
Reading the file, it looks like |
Yes, with leanprover/lean4#2452 there would have been no issue here. |
Pull request successfully merged into master. Build succeeded: |
…ha n) (#10637) A global `variable {m : Sym α n}` was present in `Mathlib.Data.Finset.Sym` with the very unfortunate effect that docs#Finset.sym_eq_empty was using it : ``` theorem Finset.sym_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {n : ℕ} {m : Sym α n} : Finset.sym s n = ∅ ↔ n ≠ 0 ∧ s = ∅ ``` thus making it impossible to use to prove its goal. The line is modified, added in a few functions when needed. Co-authored-by: Antoine Chambert-Loir <[email protected]>
…ha n) (#10637) A global `variable {m : Sym α n}` was present in `Mathlib.Data.Finset.Sym` with the very unfortunate effect that docs#Finset.sym_eq_empty was using it : ``` theorem Finset.sym_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {n : ℕ} {m : Sym α n} : Finset.sym s n = ∅ ↔ n ≠ 0 ∧ s = ∅ ``` thus making it impossible to use to prove its goal. The line is modified, added in a few functions when needed. Co-authored-by: Antoine Chambert-Loir <[email protected]>
A global
variable {m : Sym α n}
was present inMathlib.Data.Finset.Sym
with the very unfortunate effect that docs#Finset.sym_eq_empty was using it :thus making it impossible to use to prove its goal.
The line is modified, added in a few functions when needed.