The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Basically, whenever you start running into problems with coq's intensional equality. Coq makes the trade off of intensional equality for decidable type checking, but there are always sticky situations where you need more elaborate representations, hence setoids.

On Dec 29, 2012 2:49 PM, "Victor Porton" <porton AT narod.ru> wrote:

http://www.cs.berkeley.edu/~megacz/coq-categories/ uses setoids.

http://www.seas.upenn.edu/~cis500/current/sf/Rel.v does not use setoids.

Why these are different with their basic underlining data types?

In which cases setoids should be used and in which not?

--
Victor Porton - http://portonvictor.org