coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Extraction of existentially quantified variables

From: Andrej Bauer <andrej.bauer AT andrej.com>
To: Adam Chlipala <adamc AT csail.mit.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Extraction of existentially quantified variables
Date: Fri, 10 Feb 2012 21:56:25 +0100

Since we are on this topic, can someone please explain to me why Coq
even bothers with the ugly Obj.t and __? Why not just delete the
irrelevant stuff instead of dragging it along? My reasoning would be:
things outside of Set cannot be computed with, so we convert them all
to unit. We did something like that in RZ.

With kind regards,

Andrej

[Coq-Club] Extraction of existentially quantified variables, AUGER Cédric
- Re: [Coq-Club] Extraction of existentially quantified variables, Adam Chlipala
  - Re: [Coq-Club] Extraction of existentially quantified variables, Andrej Bauer
    - Re: [Coq-Club] Extraction of existentially quantified variables, AUGER Cédric
      - Re: [Coq-Club] Extraction of existentially quantified variables, Andrej Bauer
        
        Re: [Coq-Club] Extraction of existentially quantified variables, Stéphane Glondu
        
        Re: [Coq-Club] Extraction of existentially quantified variables, Andrej Bauer
        
        Message not available
        
        Re: [Coq-Club] Extraction of existentially quantified variables, Bruno Barras
        Re: [Coq-Club] Extraction of existentially quantified variables, Andrej Bauer