The Coq mailing list

[rk1 <rkam2001 AT hotmail.com>]

Although I've run across these two things before in my learning Coq, I still
don't really know what the difference is.  The main issue that's prompting
my question is that in a particular library I have a bijective Map from one
setoid to another.  I figured it'd be easy to create the inverse map --
wrong!  Because bijectivity is defined with "exists", I can't elim it to
"instantiate" the preimages to define the inverse map.  The error Coq gives
is:

"User error: Cannot find the elimination combinator ex_rect
The elimination of the inductive definition ex_rect on sort Type is not
allowed"

I have the feeling that if the maps were defined using sigT instead of
exists, I might be able to do what I want.  Is that correct?
-- 
View this message in context: 
http://www.nabble.com/Difference-between-exists-and-sigT-tf3869234.html#a10962330
Sent from the Coq mailing list archive at Nabble.com.