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.
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?
Check or Compute not Print
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