The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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?