The Coq mailing list

[roconnor AT theorem.ca]

I've declared a setoid relation:

Relation (ms,ms_eq);

where ms: MetricSpace -> Type
and ms_eq: forall m : MetricSpace, ms m -> ms m -> Prop

I haven't been able to get setoid_rewrite to work on instances of this.

Even the most simple case:

x : ms R
y : ms R
______________________________________(1/2)
@ms_eq R x y

setoid_replace x with y.

generates the goal:

______________________________________(2/3)
@eq (ms R) y x

instead of @ms_eq R y x.

I've tried

setoid_replace x with y using relation ms_eq.

which gives the error message: ``User error: Not a proposition or a type''

and I've tried

setoid_replace x with y using relation (@ms_eq R).

which gives the error message: ``User error: @ms_eq R is not a registered 
relation.''

How do I use setoid_rewrite with parametric relations?

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''