Stream: Coq users

Topic: Vector and Fin questions

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 $p \in 0..N$ it should return $S p \in 0..S N$. Or, better yet, is there a more advanced vector library somewhere with richer API and more lemmas?

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)

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: Oct 13 2024 at 01:02 UTC