Dubravka Kutlesic (Oct 20 2021 at 10:42): Dubravka Kutlesic (Oct 20 2021 at 10:42):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!
Ali Caglayan (Oct 20 2021 at 12:48):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: Oct 03 2023 at 02:34 UTC