coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prop, Set, Type and list

From: Julien Tesson <julien.tesson AT univ-orleans.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Prop, Set, Type and list
Date: Wed, 13 Jul 2011 10:53:52 +0200

Thank you for your clear answer :)

The only thing I miss is an example of extracted program where a structure
containing only elements in Prop would be really meaningful, but I am sure
that such thing exists ....

[Coq-Club] Prop, Set, Type and list, Julien Tesson
- <Possible follow-ups>
- Re: [Coq-Club] Prop, Set, Type and list, brandon_m_moore
  - Re: [Coq-Club] Prop, Set, Type and list, Julien Tesson
    - Re: [Coq-Club] Prop, Set, Type and list, AUGER Cedric
      - Re: [Coq-Club] Prop, Set, Type and list, Julien Tesson
        
        Re: [Coq-Club] Prop, Set, Type and list, AUGER Cedric
        
        Re: [Coq-Club] Prop, Set, Type and list, Julien Tesson
        
        Re: [Coq-Club] Prop, Set, Type and list, Guillaume Melquiond