coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Existential instantiation with addition information

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Existential instantiation with addition information
Date: Thu, 26 Nov 2015 17:40:23 +0100

On 26/11/2015 17:39, Dominique Larchey-Wendling wrote:
> Or maybe he can replace his argument with a proof by well-founded
> induction over lt (< on nat) ? And this wouldn't require decidability
> of P.

Indeed, this looks more idiomatic in Coq.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Existential instantiation with addition information, David Asher, 11/26/2015
- Re: [Coq-Club] Existential instantiation with addition information, Adam Chlipala, 11/26/2015
- Re: [Coq-Club] Existential instantiation with addition information, Pierre-Marie Pédrot, 11/26/2015
  - Re: [Coq-Club] Existential instantiation with addition information, Dominique Larchey-Wendling, 11/26/2015
    - Re: [Coq-Club] Existential instantiation with addition information, Pierre-Marie Pédrot, 11/26/2015
  - Re: [Coq-Club] Existential instantiation with addition information, Xavier Leroy, 11/26/2015
  - Re: [Coq-Club] Existential instantiation with addition information, Jean-Francois Monin, 11/26/2015
    - Re: [Coq-Club] Existential instantiation with addition information, Jean-Francois Monin, 11/26/2015
  - Re: [Coq-Club] Existential instantiation with addition information, Arnaud Spiwack, 11/26/2015
    - Re: [Coq-Club] Existential instantiation with addition information, Arnaud Spiwack, 11/28/2015