The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi Adam,

On Mon, Mar 02, 2009 at 06:44:35PM -0500, Adam Chlipala wrote:
> Ian Lynagh wrote:
> >I'm very new to coq, and am trying to do some proofs with C-zar.
> 
> I've never heard of C-zar,

http://coq.inria.fr/V8.2/doc/html/refman/Reference-Manual014.html

> but here's a normal Ltac proof.

Thanks for the proof, but unfortunately I don't consider Ltac proofs
readable, which is why I'm trying to use C-zar.


Thanks
Ian