Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

doc: list default settings and how to override them in the manual #540

Merged
merged 1 commit into from
Oct 21, 2024
Merged

doc: list default settings and how to override them in the manual #540

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions vscode-lean4/manual/manual.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,17 @@ Settings of the Lean 4 VS Code extension and VS Code itself can be configured in

The specific settings of the Lean 4 VS Code extension are described in detail in later sections.

The Lean 4 VS Code extensions sets a number of default settings for Lean 4 documents:
- **'Editor: Insert Spaces': true**. Pressing `Tab` will insert spaces.
- **'Editor: Tab Size': 2**. Pressing `Tab` will insert two spaces.
- **'Files: Encoding': UTF-8**. Files use the [UTF-8 encoding](https://en.wikipedia.org/wiki/UTF-8).
- **'Files: Eol': \n**. All lines use `\n` as the line break symbol for consistency between Windows and Unix based operating systems.
- **'Files: Insert Final Newline': true**. All files are terminated by an empty line.
- **'Files: Trim Final Newlines': true**. There is only a single empty line at the end of each file.
- **'Files: Trim Trailing Whitespace': true**. There is no redundant whitespace at the end of a line.

It is recommended to leave these settings at their default. Nonetheless, these default settings can be overriden in the ['Settings' page of VS Code](command:workbench.action.openSettings2) by first entering `@lang:lean4` into the settings search bar and then changing the respective setting.

<br/>

| ![](images/settings_page.png) |
Expand Down
Loading