Hi, I want to define a class with an arbitrary number of functions (f) for which the same properties hold. I would like to have a parameter n that says how many functions I will have, and after I would like to write stuff in a manner for all i in {1,..,n} it holds that " .. f(i) .." and also for every j!=i: it holds that "... f(i) .. f(j)..". Thanks in advance!

If you know that the types of `f`

are the same, then you can use vectors: https://coq.inria.fr/library/Coq.Vectors.VectorDef.html

Last updated: Feb 05 2023 at 22:03 UTC