LSP-lean

Lean support for Sublime’s LSP plugin

Uses Lean to provide completions, validation, and other features for lean code.

Installation

1. Install LSP and LSP-lean from Package Control.
2. Restart Sublime Text.

undefinedNoteundefined

1. Make sure you have already installed lean, such that the command works and is accessible from your PATH.
2. The lean language syntax definition is provided separately as the Lean package in Package Control.

Configuration

Open configuration file by running Preferences: LSP-lean Settings from Command Palette
or via Main Menu (Preferences > Package Settings > LSP > Servers > LSP-lean).