Timeline for Euclidean Algorithm in Coq
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 12, 2013 at 23:42 | comment | added | Luke Mathieson | @user11942 In addition to Coq'Art, I also strongly recommend the starting chapters of Software Foundations. It takes you through a lot of this stuff, with inline examples and exercises - it's really aimed at teaching Coq from absolute basics. It also has the advantage of being free! | |
| Dec 12, 2013 at 23:41 | comment | added | Luke Mathieson | @user11942 I just want to (explicitly) second the advice in Cody's answer. Particularly point 2, and the logical extension of it. A lot of the pieces you're putting together have already been done, in largely or exactly the same way, but have the advantage that they're properly integrated with the tactic library. | |
| Dec 12, 2013 at 23:41 | comment | added | user11942 | Thanks @cody! I will most certainly take your advice and subscribe to the mailing list $\textbf{and}$ do less ambitious projects. As you said, it is far more challenging (at least for a beginner like myself) to prove Euclidean division in Coq then on paper. | |
| Dec 12, 2013 at 20:56 | history | edited | cody | CC BY-SA 3.0 |
Elaboration
|
| Dec 12, 2013 at 20:06 | history | answered | cody | CC BY-SA 3.0 |