The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Gilbert,

> Add Ring ModRing3 : ModRing3 (decidable Mod3Dec_correct).

thanks a lot for this hint, very useful!

I wouldn't have interpreted the description of "decidable" in the manual in 
this way since something like (mulmod 3 4 x) cannot be simplified by 
computation if x is unknown. I must admit, most of the other options are also 
not that easy to understand for me either.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928