coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Conditioning notations on whether something is in [Prop] or in a larger [Type].

From: Bas Spitters <spitters AT cs.ru.nl>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: 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 09:24:03 +0200

On Wed, Aug 29, 2012 at 7:45 AM, Jason Gross
<jasongross9 AT gmail.com>
wrote:
> I'm trying to generalize some of the standard library constructs to permit
> the use of [Type] rather than [Prop] (in particular, the structures that are
> behind the scenes of [reflexivity], [transitivity], [symmetry], [Add
> Parametric Relation], [Add Parametric Morphism], and
> [rewrite]/[setoid_rewrite]).

Some of these issues have been resolved when using [identity] instead of [eq].

Bas

[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