Stream: Coq users

Topic: How to define function


view this post on Zulip sara lee (Apr 28 2022 at 03:40):

I have defined a function f with input arguments a(nat) & list nat(l1) and output list nat(l).Main function of f is to execute f1. Variable a is used by function f1 within f. Function f1 performs its functionality by using same a and increment the variable a by 1.Then assign new value to a again(a is initially zero).
a=f1(a l1). when a=lenght(l1) then f1 reset a=0. Therefore f is converging.
During each recursive call I want to store a in output list and then count it at the end of program. I have problem that i cannot use repeat function due to changing value of a during each iteration and control of recursive call(which should be greater than 1).
Please anybody like to help me in writing this function. I will be very thankful.


Last updated: Apr 19 2024 at 06:02 UTC