The Coq mailing list

[Dimitris Vekris <dvekris AT hotmail.com>]

Could you give me a hint cause i'm stuck?

Lemma lemma1 (ord : nat)(sl : list ST)(l : nat) :
                 find ord sl (S l) = S (find ord sl l).
Proof.
intros.
induction sl; simpl.
reflexivity.
destruct (compare_nat (order a) ord).
Admitted.

Thanks for your help!

> CC: coq-club AT pauillac.inria.fr
> From: devriese AT cs.tcd.ie
> To: dvekris AT hotmail.com
> Subject: Re: [Coq-Club] Problems with tail-recursion.
> Date: Thu, 12 Mar 2009 15:11:03 +0000
>
> What's difficult about them? I tried lemma1 and lemma2, and they go
> through easily enough. Where do you get stuck?
>
> (BTW, compare_nat is eq_nat_dec from the Arith library).
>
> Edsko

---

What can you do with the new Windows Live? Find out