The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Jan 5, 2016, at 21:46 , Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Sorry, I forgot that I had to make another fix to your code.

Thanks! That was it. Now about your other suggestion:

1) Take a look at  MathClasses.theory.setoids.ext_equiv_refl 

Moreover, you might want to reuse MathClasses.interfaces.abstract_algebra.Setoid_Morphism instead of defining your own `O`.

That was also super helpful! I still want to have my own class but I just defined it as:

  Class O (op: A -> A) :=

    o_setoidmor :> Setoid_Morphism op.

and if I use `apply ext_equiv_refl` instead of `reflexivity` everything works just great. Here is full example: http://ideone.com/rbD6rv reworked per your suggestions.

However I am still wondering if there is a way to declare such refined/specialized instance of ‘Reflexive’ for Setoid_Morphisms so 

reflexivity tactics would work as well?

Sincerely,
Vadim Zaliva

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

Skype: vzaliva