2025-04-20.
- solved the first file in a lean tutorial.
- The Lean plugin of vscode is quite smooth.
- In terms of silently setting up the necessary build systems, executables and libraries,
- and in terms of showing interesting things when the cursor is within a term or in a tactic.
- The Lean plugin of vscode is quite smooth.
- also solved the second file.
- the last exercise was a bit fun.