The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello,

I have a fixpoint with "fuel" argument (i.e. argument which restricts depth of recursion).
Then I have a proof that for any argument of this fixpoint there is such "fuel" value, that
the fixpoint suceeds.

Fixpoint f (x : X) (n : nat) : option Y := ...
Lemma termination : forall x, exists n y, f x n = Some y.

But then I somehow can't invent a way to compose then into "good" fixpoint:

Fixpoint f' (x : X) : Y.

Could anybody prompt me how to incorporate the proof into "good" fixpoint?

Sincerely,
Kirill Taran