Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page