Vector Repr instance

Stream: lean4

[Wrenna Robson]

Would it be possible to change the Repr instance for Vector? It is currently the default one, which isn't very useful - it just prints the array along with useless stuff. It would be more useful to have it in the form #v[3, 4, 5], say.

[Wrenna Robson]

I would make the change myself, but I think Vector is now defined in core along with its Repr instance, so I'm a bit scared about touching it!

[Wrenna Robson]

(It seems like the procedure for core is that I need to create an RFC?)

[Shreyas Srinivas]

I think you can make a batteries PR

[Shreyas Srinivas]

Then core can take it when they want to.

[Shreyas Srinivas]

CC : @François G. Dorais

[Wrenna Robson]

Right, but as core already has a Repr instance (it auto-derives it), won't it clash if it's in batteries?

[Shreyas Srinivas]

Oh right

[Wrenna Robson]

What would be useful is core simply removing the Repr auto-derivation and then we work on the alternative in batteries. But still requires a change to core! I don't understand why they imported the default one.

[Shreyas Srinivas]

That little fiasco might be my fault since I didn't create a proper Repr instance, and then it got upstreamed. But I also recall that #eval wasn't using unexpanders back then

[Wrenna Robson]

I am afraid I don't know what an unexpander is :)

[Edward van de Meent]

there is a small paragraph about it in the metaprogramming book