Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Problems with tail-recursion.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problems with tail-recursion.


chronological Thread 
  • From: Edsko de Vries <devriese AT cs.tcd.ie>
  • To: dimitrisg7 <dvekris AT hotmail.com>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Problems with tail-recursion.
  • Date: Thu, 12 Mar 2009 15:11:03 +0000
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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





Archive powered by MhonArc 2.6.16.

Top of Page