Stream: Coq users

Topic: Input and output relation

view this post on Zulip zohaze (Apr 03 2022 at 10:00):

I have model a system in Coq. The input to this model is list of natural numbers. I want to repeat the output of model against the input of same type but different value for 3 or 4 time. I don't know the command which i should apply here,so that same model may be use multiple time against varying input of same type. Please guide me.

view this post on Zulip Andrew Hirsch (Apr 03 2022 at 14:43):

I'm not sure I understand your question. It sounds like you have a function written in Coq that you want to apply to two different lists of numbers. If you want to see the output of such a function, you can just write Print (f list1). Print (f list2). to see the output of both function calls.

If there's something more complicated going on, can you explain in a bit more detail?

view this post on Zulip Gaëtan Gilbert (Apr 03 2022 at 15:18):

Check or Compute not Print

view this post on Zulip zohaze (Apr 04 2022 at 17:40):


Last updated: Oct 03 2023 at 21:01 UTC