Stream: Coq users

Topic: Vector and Fin questions


view this post on Zulip k32 (Aug 09 2020 at 11:09):

Hello! I am trying to utilize Vectors.Fin module from the standard library, but documentation is a bit scarce. Is there a function that increments values of Fin.t type? E.g. given p0..Np \in 0..N it should return Sp0..SNS p \in 0..S N. Or, better yet, is there a more advanced vector library somewhere with richer API and more lemmas?

view this post on Zulip Karl Palmskog (Aug 09 2020 at 11:28):

we have an alternative representation of Fin here (without vectors), not exactly sure how the lemma collection compares to Stdlib: https://github.com/uwplse/StructTact/blob/master/theories/Fin.v --- and there is also the one in stdpp: https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/theories/fin.v (they have their own vector library)

view this post on Zulip Paolo Giarrusso (Aug 09 2020 at 19:41):

FWIW, stdpp's fin and vector library extend the stdlib with extra facts and notation, so you can still use everything from the stdlib


Last updated: Feb 06 2023 at 00:03 UTC