Reading a Lean Project

Planned post. This page is a stub.

Toolchains, Lake, imports, namespaces, and finding definitions.

Planned Coverage

Trace a definition through imports and identify which build targets check it.

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