The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Is it possible to do something like:

Definition assert (b : bool) : Prop := (b = true).

Coercion assert : bool >-> Prop.

I get the following error (in Coq 8.4pl2) :

Syntax error: [vernac:class_rawexpr] expected after '>->' (in [vernac:gallina_ext]).

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/