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:30:43 +0100

Thanks! The proof became very short thanks to the derrived pick_equation! I
assume this is how one usually does recursive functions - I'm still learning,
so thank you a lot!

[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