This appendix is the only place in the course that names tools. Everything before it spoke of the formal tool, the solver and the front-end option; here those map to concrete programs so that you can rerun a proof on your own machine. The topic hub itself names nothing: the one lesson that names tools carries the Appendix label at its top.
Lesson | After it you can... |
|---|---|
Install the flow, map a proof header to a project file and commands, and read the output. | |
Extend the lab with ten exercises and file each in the ledger. |
Suggested order: the flow lesson first, with a terminal open; the exercises second, each filed as a ledger row before the next is started.
So every other lesson stays true on any formal tool: names would tie the argument to one installation, while concepts transfer everywhere.