unexpected breakage from a PR

Stream: general

[Mantas Baksys]

In my commit #10889, mathlib unexpectedly won't build. The breakage is at set_theory/game/domineering, (I presume) because of an unexpected lex.decidable_eq instance in line 98. Can someone help explain what happened here and how to fix this? Thanks

[Yaël Dillies]

To add more information, this PR adds an import of order.lexicographic, so I suspect it is a transparency problem of docs#lex which happens to have gone unnoticed so far.

[Eric Wieser]

It would be good to add a prod.to_lex and lex.to_prod def somewhere, rather that relying on @s to convert between types

[Eric Wieser]

(out of scope for that PR, but worth doing at some point)

[Yaël Dillies]

I was wondering whether switching to the architecture I use in data.sigma.order might be better. Another option is to have lex α a type synonym of α and put lexicographical instances on lex (α × β), lex (Σ i, α i), lex (Σ' i, α i).

[Yaël Dillies]

Which one do you prefer?

[Eric Wieser]

I quite like the single type synonym approach you're suggesting there

[Yaël Dillies]

Me too. I'll refactor then. Where should the type synonym be defined? I think it could go in order.lexicographic (which I'm planning to rename in data.prod.lex or data.prod.order at some point).