coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "Function {measure}" and induction principles

From: Chris Casinghino <chris.casinghino AT gmail.com>
To: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
Cc: David Pichardie <david.pichardie AT inria.fr>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] "Function {measure}" and induction principles
Date: Wed, 29 Jun 2011 09:49:47 -0700

Hi Cedric, David and Pierre,

Thanks for the wonderful responses! All three examples were very
helpful, and this simplifies my development dramatically.

--Chris

[Coq-Club] "Function {measure}" and induction principles, Chris Casinghino
- Re: [Coq-Club] "Function {measure}" and induction principles, AUGER Cedric
  - Re: [Coq-Club] "Function {measure}" and induction principles, Pierre Courtieu
  - Re: [Coq-Club] "Function {measure}" and induction principles, Pierre Courtieu
- Re: [Coq-Club] "Function {measure}" and induction principles, David Pichardie
  - Re: [Coq-Club] "Function {measure}" and induction principles, Pierre Courtieu
    - Re: [Coq-Club] "Function {measure}" and induction principles, Chris Casinghino