The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

It is no longer important. I just forgot about the composition of functions.
Thanx to Jonas Oberhauser. He understood what I need.

Greetings,

Marko Malikovic
> Marko Malikoviæ wrote:
>> No,
>>
>> I ask whether it is possible to create a function Change2 that will be
>> defined as "Change1 (Change1 SomeTuple)" but without the use of
>> induction.
>> So, the function which will two (or more) times in the same way change
>> the
>> tuple. So Change1 function must return a result that is the same type as
>> its argument.
>> Something like this:
>>
>> Definition Change2 (TupleB): = Change1 (Change1 TupleA).
>>
>
> I'm still having trouble identifying some non-trivial issue in your
> question.  Are you asking how to write a recursive function in Coq?  Or
> when you write "induction" do you mean "recursion," such that you are
> looking for a way to implement an iterated self-composition function
> without explicit recursion?