Dfinsupp.Lex

Stream: mathlib4

[Yury G. Kudryashov]

I tried porting data/dfinsupp/well_founded and many lemmas fail because it can't figure out i in s : ∀ {i}, α i → α i → Prop.

[Yury G. Kudryashov]

@Jason Yuen What was the reason to go from ∀ i, α i → α i → Prop to ∀ {i}, α i → α i → Prop?

[Eric Wieser]

(port-status#data/dfinsupp/well_founded)

[Eric Wieser]

What was the reason to go from ∀ i, α i → α i → Prop to ∀ {i}, α i → α i → Prop?

I'm confused, the lean3 file seems to only use the first spelling?

[Eric Wieser]

Oh, you're referring to https://github.com/leanprover-community/mathlib4/pull/2199/files#diff-c4e63f77fa4be2d3e0e3051c0d8f76060089bca33778465a952920efe51036f9R34

[Yury G. Kudryashov]

Should I revert this API change?

[Eric Wieser]

I think we should at least try to revert it, and if we discover why that's hard add a better porting note

[Jason Yuen]

Yury G. Kudryashov said:

Jason Yuen What was the reason to go from ∀ i, α i → α i → Prop to ∀ {i}, α i → α i → Prop?

Sorry for the super late response. I think I made this change because it made porting the file more convenient. It's probably safe to revert it to ∀ i.

[Yury G. Kudryashov]

I'll look at this again tomorrow.