Source-only fixture. Compilation has not been executed. In an isolated Lean 4.19.0 environment: lean Main.lean.