coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] UIP and decidable equality

From: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] UIP and decidable equality
Date: Tue, 13 Sep 2016 19:00:37 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 18.mo4.mail-out.ovh.net
Ironport-phdr: 9a23:V8NHyhLFpO3TGpMPZdmcpTZWNBhigK39O0sv0rFitYgXLfzxwZ3uMQTl6Ol3ixeRBMOAuqsC1LKd4vuoGTRZp83e4DZaKN0EfiRGoPtVtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaymUrLV2s+wzqW5/4DZSwROnju0J71ofzusqgCEk8AGgI5vYoqwzJvS6i9NcuVS7WZhNVOWkhrx4MqrupB5pXcD88k9/tJNBP2pN58zSqZVWWwr

Hi Jonathan,

On 09/13/16 17:51, Jonathan Leivent wrote:
> it can interfere with the preservation of properties like complexity
> between extracted code and the original Coq source.

Can you elaborate a bit? I vaguely remember this being discussed on the
list at some point, but I forgot what it was about.

Thanks!

Maxime.

[Coq-Club] UIP and decidable equality, Alan Schmitt, 09/09/2016
- Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/09/2016
  - Re: [Coq-Club] UIP and decidable equality, Alan Schmitt, 09/09/2016
    - Re: [Coq-Club] UIP and decidable equality, Thorsten Altenkirch, 09/12/2016
      - Re: [Coq-Club] UIP and decidable equality, Jonathan Leivent, 09/12/2016
        
        Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/12/2016
        
        Re: [Coq-Club] UIP and decidable equality, Thorsten Altenkirch, 09/13/2016
        
        Re: [Coq-Club] UIP and decidable equality, Jonathan Leivent, 09/13/2016
        Re: [Coq-Club] UIP and decidable equality, Maxime Dénès, 09/13/2016
        Re: [Coq-Club] UIP and decidable equality, Jonathan Leivent, 09/13/2016
        Re: [Coq-Club] UIP and decidable equality, Maxime Dénès, 09/13/2016
        Re: [Coq-Club] UIP and decidable equality, Pierre-Marie Pédrot, 09/13/2016
        
        Re: [Coq-Club] UIP and decidable equality, Jonathan Leivent, 09/13/2016
        
        Re: [Coq-Club] UIP and decidable equality, Thorsten Altenkirch, 09/13/2016
      - Re: [Coq-Club] UIP and decidable equality, Alan Schmitt, 09/13/2016
- RE: [Coq-Club] UIP and decidable equality, Soegtrop, Michael, 09/09/2016
  - Re: [Coq-Club] UIP and decidable equality, Alan Schmitt, 09/09/2016
- Re: [Coq-Club] UIP and decidable equality, Jonathan Leivent, 09/09/2016
  - Re: [Coq-Club] UIP and decidable equality, Jason Gross, 09/09/2016