Stream: Coq users

Topic: class with chosen number of functions


view this post on Zulip 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!

view this post on Zulip 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: Feb 05 2023 at 22:03 UTC