The stdlib arrays library is not very extensive.
This one is nice, but a bit dated. Are there better options? Should some library of arrays be included in platform?
It would be especially nice to have a good library which has compatible native and elementary implementations, so that one can use the native version for interactive development and the elementary one for offline checks without the axioms.
I agree, do you want me to open an issue in platform, so we record this?
coq-array only compiles with master at the moment...
I am not so sure if this is something which should go into platform or the standard library. Since we now have native arrays, my opinion is that something basic to use this does belong in the standard library.
Perhaps I am misunderstanding what you are saying, but, as far as I know,
coq-array provides plain lists, which are completely unrelated to Coq's native arrays.
@Guillaume Melquiond indeed, there are two observations. The stdlib is not very extensive, and coq-array is available.
I believe one would like to connect them via an isomorphism, or perhaps refinement.
Last updated: Jan 27 2023 at 01:03 UTC