lean.nvim

<div align="center">
  <div>
    <div><img alt="lean.nvim" src="https://github.com/user-attachments/assets/727b689d-56f6-48e8-8fe5-a7a5d82b91c5" width="400px"/></div>
    <div><h1>lean.nvim</h1></div>
  </div>
  <table>
    <tr>
      <td>
        <strong><a href="https://neovim.io">Neovim</a> support for the <a href="https://lean-lang.org/">Lean Theorem Prover</a></strong>
      </td>
    </tr>
  </table>

[![Lua](https://img.shields.io/badge/Lua-blue.svg?style=for-the-badge&logo=lua)](http://www.lua.org)
[![Neovim](https://img.shields.io/badge/Neovim%200.11+-green.svg?style=for-the-badge&logo=neovim)](https://neovim.io)
[![MIT](https://img.shields.io/badge/MIT-yellow.svg?style=for-the-badge)](https://opensource.org/licenses/MIT)
<a href="https://dotfyle.com/plugins/Julian/lean.nvim">
<img alt="dotfiles using lean.nvim" src="https://dotfyle.com/plugins/Julian/lean.nvim/shield?style=for-the-badge" />
</a>

</div>

https://github.com/user-attachments/assets/d17554ae-bcce-4f73-ac34-38ae556caf45

## Installation

If you are using neovim 0.12 or later, you can install and configure `lean.nvim` using

```lua
vim.pack.add { "https://github.com/Julian/lean.nvim" }

vim.g.lean_config = { mappings = true }
```

(see [the manual](https://github.com/Julian/lean.nvim/wiki/The-lean.nvim-Manual#key-mappings) for information about the `{ mappings = true }` part).

If you are using an older neovim, or do not wish to use `vim.pack`, `lean.nvim` can be installed via your favorite plugin manager.
Here's an example doing so with [lazy.nvim](https://github.com/folke/lazy.nvim):

```lua
{
  'Julian/lean.nvim',
  event = { 'BufReadPre *.lean', 'BufNewFile *.lean' },

  dependencies = {
    -- optional dependencies:

    -- 'nvim-telescope/telescope.nvim', -- for Lean-specific pickers
    -- 'andymass/vim-matchup',          -- for enhanced % motion behavior
    -- 'andrewradev/switch.vim',        -- for switch support
    -- 'tomtom/tcomment_vim',           -- for commenting
  },

  ---@type lean.Config
  opts = { -- see the manual for full configuration options
    mappings = true,
  }
}
```

`lean.nvim` supports the latest stable neovim release (currently `0.12.x`) as well as the latest nightly.
If you are on an earlier version of neovim, e.g. `0.10.x`, you can have your plugin manager install the [`nvim-0.10` tag](https://github.com/Julian/lean.nvim/releases/tag/nvim-0.10) until you upgrade.

### Optional: Terminal Graphics

In terminals that support the [Kitty graphics protocol](https://sw.kovidgoyal.net/kitty/graphics-protocol/) (Kitty, WezTerm, Ghostty, etc.), `lean.nvim` can render images and SVGs from ProofWidgets inline in the infoview.

SVG rendering requires [resvg](https://github.com/RazrFalcon/resvg) (`brew install resvg` or `cargo install resvg`).
Raster images (`<img>` tags with data URIs) work without any extra dependencies.

To disable all terminal graphics, set `graphics = { enabled = false }` in your configuration.

## Sponsors

A portion of `lean.nvi