data.typevec

Stream: mathlib4

[Jireh Loreaux]

If anyone wants to have a look at mathlib4#891 I would appreciate it. It's a huge mess. I think it's due to the fact that we have to deal with type equalities in various places and I think there's plenty of defeq abuse going on in the mathlib3 side which is causing stuff to fail arbitrarily in mathlib4. I don't think this is actually an important file, which is why I've let it sit for a while, but at this point it would just be nice to get it done.

[Jireh Loreaux]

Also the ♯ notation doesn't seem to work.

[Gabriel Ebner]

I feel like we're missing a simp lemma somewhere:

example (a b : Typevec 0) : a = b := by simp -- should work

[Gabriel Ebner]

And @Mario Carneiro removed that simp lemma: https://github.com/leanprover/std4/blob/01992b1846d5f2d1191b22032a67485d739ed8ff/Std/Logic.lean#L729

[Mario Carneiro]

This simp lemma was historically a cause of problems in lean 3 so I would like someone to make sure it won't cause the same issues in lean 4 before putting it in std

[Mario Carneiro]

I don't mind relocating this to mathlib4 if it simplifies matters for the present though

[Gabriel Ebner]

Yes, please put it back in mathlib4, with the simp attribute.