Porting Logic.Equiv.Array for Primrec

Stream: mathlib4

[Praneeth Kolichala]

It seems that computability/primrec shows that arrays are primcodable in Lean 3 (because they are equivalent to vectors/functions on fin n). However, the relevant file hasn't been ported yet and has been marked low priority. I think that arrays are not even used in computability, and that we can proceed without this dependency, but I would like to confirm with @Mario Carneiro just to be sure.

[Mario Carneiro]

The easy thing to do is to comment out the array primcodable instance

[Mario Carneiro]

I think the story with Logic.Equiv.Array is that it shouldn't be ported, it should be rewritten while keeping approximately the same theorems

[Mario Carneiro]

It's basically similar to files from std in that they are presenting a similar interface but are built on completely different primitives and so have to be mostly written from scratch