coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: gallego AT cri.ensmp.fr (Emilio Jesús Gallego Arias)
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Coercion from bool to Prop
- Date: Fri, 19 Dec 2014 18:38:26 +0100
- Cancel-lock: sha1:JAtHos+F/Z9EokPk8RUSd/yQ3so=
Abhishek Anand
<abhishek.anand.iitg AT gmail.com>
writes:
> Definition assert (b : bool) : Prop := (b = true).
> Coercion assert : bool >-> Prop.
Note that "assert" is already defined by the standard library as
"is_true" (see theories/Init/Datatypes.v).
You may want to keep using it instead of defining your own:
Notation assert b := (is_true b).
(I wonder if assert is the best name given that is also the name of a
tactic)
Best regards,
Emilio
- [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
- Re: [Coq-Club] Coercion from bool to Prop, Arthur Azevedo de Amorim, 12/18/2014
Archive powered by MHonArc 2.6.18.