bInter and mathport

Stream: mathlib4

[Yury G. Kudryashov]

Hi @Mario Carneiro , reporting another bug in mathport or mathlib 4. When it sees ⋂ j ≠ i, s j, it outputs ⋂ (j) (_ : j ≠ i), s j but mathlib4 can't parse it. I have to change it to ⋂ (j) (_hj : j ≠ i), s j (⋂ (j) (hj : j ≠ i), s j doesn't work either because of an unused named argument). Probably, it's better to fix this on the mathlib 4 side because being forced to use a name _h just to make both parser and linter happy feels strange.

[Mario Carneiro]

yeah that sounds like a bug in mathlib4

[Mario Carneiro]

or more likely lean4 core / std4

[Floris van Doorn]

We also noticed this here