The lecture notes accompanying the Basics chapter of Logical Foundations are now available.
View or download the source: BasicsLecture.v
These notes work through functional programming in Rocq — booleans, types, modules, tuples, numbers, and proof by simplification — as developed live in lecture. Load the file in VSCode with coq-lsp (or vsrocq) and step through it interactively.