Programming and Proving in Lean

Planned post. This page is a stub.

Executable definitions, propositions, proof terms, and tactics.

Planned Coverage

Connect a small function to a theorem about its result and inspect the proof state.

Examples, definitions, and exercises will be developed here as the course progresses. See the course table of contents for the suggested reading order.