coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proving a theorem about a recursive function that uses Acc

From: <lars.rasmusson AT sics.se>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proving a theorem about a recursive function that uses Acc
Date: Tue, 09 Dec 2014 12:19:56 +0100

Thanks!

I was trying to learn about using Acc, so I guess my example wasn't very well
chosen.
You make a good point about not overcomplicaticising unnecessarily... :-)

[Coq-Club] Proving a theorem about a recursive function that uses Acc, lars.rasmusson, 12/08/2014
- Re: [Coq-Club] Proving a theorem about a recursive function that uses Acc, Pierre-Marie Pédrot, 12/09/2014
  - Re: [Coq-Club] Proving a theorem about a recursive function that uses Acc, lars.rasmusson, 12/09/2014
- Re: [Coq-Club] Proving a theorem about a recursive function that uses Acc, James Wilcox, 12/09/2014
  - Re: [Coq-Club] Proving a theorem about a recursive function that uses Acc, Lars Rasmusson SICS, 12/09/2014
- <Possible follow-up(s)>
- Re: [Coq-Club] Proving a theorem about a recursive function that uses Acc, julien . forest, 12/09/2014
  - Re: [Coq-Club] Proving a theorem about a recursive function that uses Acc, lars.rasmusson, 12/09/2014