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?

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)

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: Jun 18 2024 at 09:02 UTC