The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Thanks!  Is this done mostly in ocaml?  (grepping the source tree suggests yes.)  Is it replicable in pure Coq?

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

-Jason

On Wed, Aug 29, 2012 at 3:24 AM, Bas Spitters <spitters AT cs.ru.nl> wrote:

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