plugins.lean.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.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: