Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

plugins.lean.settings.ft.default

The default filetype for Lean files.

Type: null or string or raw lua code

Default: null

Plugin default: "lean"

Declared by:

plugins.lean.settings.ft.nomodifiable

A list of patterns which will be used to protect any matching Lean file paths from being accidentally modified (by marking the buffer as nomodifiable).

By default, this list includes the Lean standard libraries, as well as files within dependency directories (e.g. _target)

Set this to an empty table to disable.

Type: null or (list of string)

Default: null

Declared by: