Bas Spitters (May 27 2021 at 10:38): Bas Spitters (May 27 2021 at 10:38):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?
https://github.com/tchajed/coq-array
Michael Soegtrop (May 27 2021 at 17:55):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.
Bas Spitters (May 28 2021 at 09:24):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...
Michael Soegtrop (May 28 2021 at 09:38):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.
Guillaume Melquiond (May 28 2021 at 09:42):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.
Bas Spitters (May 28 2021 at 09:53):@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: Apr 19 2024 at 19:02 UTC