The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

Ryan Wisnesky wrote:
> 
> Hello everyone,
> 
> In the standard library's Logic file, projection is defined as 
> Opaque/with Qed:
> 
> Theorem proj2 : A /\ B -> B.
>    Proof.
>    destruct 1; trivial.
>    Qed.
> 
> I'm wondering if there's a deep reason for not making this definition 
> transparent.  (I'd like to get at the underlying computational behavior 
> of proj2 to help simplify another proof.)
> 
> Thanks,
> Ryan Wisnesky
> 
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
> 

I don't think there is any good reason in this case, specifically the proof
is closed so changing other lemmas will not affect it.
-- 
View this message in context: 
http://www.nabble.com/Opacity-of-Logic.proj2-tp24628106p24629157.html
Sent from the Coq mailing list archive at Nabble.com.