The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

Hi everyone.
In the code that follows, I would like to substitute cheating with an object
(H: i<10). Function testing uses recursion as you can see. Therefore, this
object should be constructed recursively for every call. Is there a easy way
to do that?

Thanks in advance!

Variable cheating : forall (A : Type), A.
Implicit Arguments cheating [A].

Definition testing (P: forall i, i < 10 -> nat -> nat)  : nat.
Proof.
intros.
refine ((fix check (i : nat) : nat := 
          match i with
            | 0 => 0
            | S n => P n cheating (check n)
          end) 5).
Qed.

-----
Never say never.
-- 
View this message in context: 
http://www.nabble.com/Question-on-recursion-tp23153959p23153959.html
Sent from the Coq mailing list archive at Nabble.com.