The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

Thank you, this works.

Are lemma proved coercions considered cheating that violates Pollack
consistency?

On Sun, Jun 12, 2011 at 08:15:38AM -0400, Adam Chlipala wrote:
> Georgi Guninski wrote:
> >I have problem using a Lemma as a coercion.
> >
> >Trying this, get stuck on goal "coer a" and can't compute/unfold it:
> >
> >
> >(* Definition coer := fun a:True =>  Prop. *)
> >Lemma coer: True->Prop.
> >intro. exact True.
> >Qed.
> 
> End in [Defined] instead of [Qed], which makes the definition
> transparent instead of opaque.  This particular example would be
> much clearer as:
>     Definition coer (_ : True) := True.
> though perhaps your real example is more involved, to the point
> where tactics are called for.  Personally, I recommend never using
> tactics to define a term with computationally significant behavior.