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):

Model of system(7 segment display) is composed of multiple functions . When get proper input in the form of list then all functions in the code do their work and I get proper output. This model is composed of different functions and lemmas. In simple words it is complete code. I just want to pass new chunk of input 3 or 4 time to this model. Now want to check response of the model against different inputs.It should accept the input (because input data type is same,just there is value difference and give output). To do this what command I should apply so that I am able to use all functions of the model against different inputs of same type. (want to attach model against every input)

Last updated: Jan 31 2023 at 14:03 UTC