data.fin.vec_notation mathlib4#1741

Stream: mathlib4

[Johan Commelin]

I started this PR, but I need help with the notation.

[Johan Commelin]

There's some stuff left about:

• a Repr instance
• unsafe defs
• bit0/bit1 stuff

[Johan Commelin]

Help appreciated!

[Eric Wieser]

I can maybe take a look at the repr instance

[Eric Wieser]

Done

[Eric Wieser]

I think it's probably reasonable to comment out the two unsafe instances for now; I think has_reflect (now docs4#Lean.ToExpr) has been made redundant somehow by Qq, although I don't really understand why

[Johan Commelin]

What about the to_pexpr stuff?

[Eric Wieser]

This was all prework for my mathlib3 meta matrix PR

[Eric Wieser]

So I think commenting it out with a porting note and maybe a TODO(eric-wieser) is fine

[Eric Wieser]

I suspect the replacement is a function from fin n → Q(α) to Q(fin n → α); maybe @Gabriel Ebner can comment on what that would look like.

[Eric Wieser]

(but no need to hold up the PR for that)

[Johan Commelin]

done

[Johan Commelin]

The only stuff remaining is the bit0/bit1 warnings

[Johan Commelin]

Who's gonna merge this?

[Eric Wieser]

Should we do the backport first?

[Eric Wieser]

Otherwise we'll have porting notes that refer to something that doesn't exist any more, which is a bit confusing

[Johan Commelin]

I think the API change isn't big enough to require a backport

[Johan Commelin]

Or at least, it doesn't need to hold up the port

[Ruben Van de Velde]

@Johan Commelin I reverted the change, but now I'm not sure if I should merge it myself :)

[Yury G. Kudryashov]

I think, it's OK for you to merge it.

[Ruben Van de Velde]

Oh, bors doesn't think I can anyway