2 Resources
Before coming to class, students should install the following software:
The Proof General IDE
Company-Coq (optional, useful add-on to Proof General)
The Turning Point app (feel free to buy a clicker if preferred). Register here.
This course will be using a modified first two volumes of Software Foundations. However, there is no need to download the books as we will be releasing our modified text one chapter at a time (see the schedule).
As the course progresses, we will maintain a cheat sheet of Coq tactics that will help you write proofs. At the beginning of the course, the cheat sheet will be unavailable or empty.
Some useful Proof General key bindings:
C-c C-RET : Processes (or reverts) to the cursor
C-c C-n : Processes the next definition/element
C-c C-u : Undoes processing of the last element
C-c C-a C-a : Search command
C-c C-; : Paste results of last Search command
C-c C-d (Company-Coq only): Shows the documentation for the indentifier under the cursor.