Logic.Equiv.Array

Stream: mathlib4

[Arien Malec]

I had a look at mathlib4#1733, and the issue here is that it depends on DArray which used to be defined in core, but is no longer a thing?

In addition, mathport seems to have renamed array to Array'?

[Arien Malec]

Should this whole thing be a no-port, because the implementation of Array is so different?

[Eric Wieser]

It seems like a very low priority file to port

[Eric Wieser]

I split the mathlib3 file very recently specifically so that we didn't have to worry about porting any of this

[Eric Wieser]

I guess we should still decide eventually though