Fixed-length arrays

Stream: general

[Shelvacu]

Is there a standard type (whether in the actual stdlib or some other common library) for representing fixed-size arrays somewhat efficiently? Or should I just be using something like { xs : Array a // a.size = 5 }?

[Aaron Liu]

docs#Vector or docs#List.Vector

[Kim Morrison]

Moreover, the API for List/Array that is provided in the standard library should (nearly) all be reproduced for Vector. If you find omissions, please ping me. :-)

[Bhavik Mehta]

Some of the things around sorting are missing for Vector, eg Array.insertionSort, Array.qsort and Array.binSearch

[Kim Morrison]

Verification for Array.qsort coming soon (more as a demo of how great grind is than actually caring about qsort), and I will try to add the Vector wrappers and API along with that.

[Mario Carneiro]

I could have sworn I already submitted a proof of qsort ages ago

[Mario Carneiro]

see lean4#3933 and lean4#5346

[Shreyas Srinivas]

Bhavik Mehta said:

Some of the things around sorting are missing for Vector, eg Array.insertionSort, Array.qsort and Array.binSearch

You should be able to lift the array theorems into vectors for now. If I had to guess, that’s what the vector API will do

[Kim Morrison]

Yes, both lean#3933 and lean#5346 were sadly abandoned.

[Bhavik Mehta]

Shreyas Srinivas said:

Bhavik Mehta said:

Some of the things around sorting are missing for Vector, eg Array.insertionSort, Array.qsort and Array.binSearch

You should be able to lift the array theorems into vectors for now. If I had to guess, that’s what the vector API will do

Sure, it's not too hard to work around, but it's still an omission!

[Mario Carneiro]

Kim Morrison said:

Yes, both lean#3933 and lean#5346 were sadly abandoned.

lean4#3933 was not abandoned by me, there were some unclear blocking concerns about benchmarking despite plenty of existing benchmarks