coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: Bas Spitters <spitters AT cs.ru.nl>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Conditioning notations on whether something is in [Prop] or in a larger [Type].
Date: Wed, 29 Aug 2012 11:58:14 +0200

On 08/29/2012 10:02 AM, Jason Gross wrote:

Are there plans to generalize this feature a la [Add Parametric
Relation] and [Add Parametric Morphism]?

Matthieu Sozeau started working on this, see:

https://github.com/mattam82/Coq-misc/tree/setoidType

[Coq-Club] Conditioning notations on whether something is in [Prop] or in a larger [Type]., Jason Gross, 08/29/2012
- Re: [Coq-Club] Conditioning notations on whether something is in [Prop] or in a larger [Type]., Bas Spitters, 08/29/2012
  - Re: [Coq-Club] Conditioning notations on whether something is in [Prop] or in a larger [Type]., Jason Gross, 08/29/2012
    - Re: [Coq-Club] Conditioning notations on whether something is in [Prop] or in a larger [Type]., Bas Spitters, 08/29/2012
      - Re: [Coq-Club] Conditioning notations on whether something is in [Prop] or in a larger [Type]., Jason Gross, 08/29/2012
    - Re: [Coq-Club] Conditioning notations on whether something is in [Prop] or in a larger [Type]., Robbert Krebbers, 08/29/2012