The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I have not looked at your code, but error messages about products generally indicate that you gave it a function where it was not expecting one, or vice versa.  (Function types are also called pi types or dependent products.)

-Jason

On Aug 28, 2013 12:19 AM, "t x" <txrev319 AT gmail.com> wrote:

Hi,

  Here is my minimal failure example:

https://gist.github.com/anonymous/df6b5d1cf5a81592ea4d

  I'm trying to build a variant of "<-" of the Maybe Monad where I can pull out either a Z or a Bool.

  However, I'm getting an error about some "product" rather than a myOpt.

  What am I doing wrong, and how do I fix this?

Thanks!