coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coercion from bool to Prop

From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Coercion from bool to Prop
Date: Thu, 18 Dec 2014 12:14:31 -0500

Just do bool >-> Sortclass instead.

On Dec 18, 2014 12:13 PM, "Abhishek Anand" <abhishek.anand.iitg AT gmail.com> wrote:

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/

[Coq-Club] Coercion from bool to Prop, Abhishek Anand, 12/18/2014
- Re: [Coq-Club] Coercion from bool to Prop, Arthur Azevedo de Amorim, 12/18/2014
  - Re: [Coq-Club] Coercion from bool to Prop, Abhishek Anand, 12/18/2014
- Re: [Coq-Club] Coercion from bool to Prop, Emilio Jesús Gallego Arias, 12/19/2014