Talk:Coq

From Wikipedia, the free encyclopedia

[edit] Confusing

This article has several definitions, whch are confusing on their own, and are not seperated. Fatalserpent 04:23, 21 May 2006 (UTC)

[edit] Diagrams/Examples

Would it be worthwhile to add some example Coq scripts, with proofs and brief explantions. Possibly to show what can be proved (including principles of classical logic as opposed to modern prop too?), and various constructs within Coq such as inductive/fixpoint definitions (Peano numbers and trees strike me as suitable candidates)? I'm aware that this article shouldn't read like a Coq tutorial, but it may help to show the readers what Coq looks like, and what it's capable of. Pyrre (talk) 03:40, 23 December 2007 (UTC)