TCS COURSE, PART 2: LOGIC AND THEOREM PROVING WITH COQ
The lecture notes that we will use for this second part of the course are available via the menu "Coq lecture notes" to your left.
The file "lecture_code.v" is the Coq file that I am developing in class during my lectures. To open this file in Coq in a Windows workstation, assuming Coq is installed, should be possible simply by clicking on the file. In a Linux workstation, open a shell, and type
coqide lecture_code.v &
which should open the file in CoqIDE.
In case of problems contact your instructor.
Lecture 9: Intro to Logic and Theorem Proving with Coq