From browser to a Lean project

Transfer the same workflow to elan, Lake, and VS Code.

8 minBeginner

0/7 completed in this course

Lean workspaceWrite only the proof steps. The theorem above is fixed.

Enter after constructor adds both goal bullets

Exercise.leanLean 4.30.0

Loading editor…

No problems detected so far. Run a check to hear from Lean.

ReadyLn 1, Col 1Pre-check passedLean 4