Stream: Coq users

Topic: Arrays


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jan 27 2023 at 01:03 UTC