The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

On Tue, Mar 03, 2009 at 08:46:37AM -0500, Adam Chlipala wrote:
> Ian Lynagh wrote:
> >On Mon, Mar 02, 2009 at 06:44:35PM -0500, Adam Chlipala wrote:
> >  
> >Thanks for the proof, but unfortunately I don't consider Ltac proofs
> >readable, which is why I'm trying to use C-zar.
> 
> Well, your particular theorem is so obviously true that I think no 
> mathematician would bother to spell out a proof in structural detail, so 
> it's unclear to me why you want to do so here.

Yes, this example is trivial, but I am working towards bigger things.
And if I can't do trivial proofs then I have no hope of doing more
complex ones!


Thanks
Ian