Lean 4 VS Code 扩展：安装与使用指南

Lean 4 VS Code扩展为Lean 4定理证明器和编程语言提供了强大的支持。本文将详细介绍如何安装和使用此扩展，帮助您快速上手Lean 4。

安装Lean 4

安装此扩展后，系统会自动打开一个包含设置指南的“欢迎”页面。该指南提供了不同平台的具体信息，涵盖以下主题：

• 书籍和文档资源
• 安装Lean所需的依赖项
• 安装Lean的版本管理器Elan以及最新稳定的Lean 4版本
• 设置Lean 4项目
• 故障排除

如果设置指南未自动打开，您可以通过以下步骤手动打开：打开一个空文件，点击右上角的∀符号，然后选择“文档…” > “文档：显示设置指南”。

使用此扩展

Lean 4 VS Code扩展手册提供了对扩展所有功能的完整且详细的概述。如果您是Lean的新手，建议阅读手册中“与Lean文件交互”部分的前五个小节，这些内容将非常有帮助。

通过本指南，您可以轻松掌握Lean 4 VS Code扩展的安装和使用方法，快速进入Lean 4的学习和开发之旅。