---

Ⅰ. 插件描述

Lean Theorem Prover plugin for Vim.

Ⅱ. 基本信息

创建日期：  2016-08-22 使用用户：  3 Github星：  4 插件作者：  Mitchell Kember

Ⅲ. 安装方法

使用Vundle管理器安装

在你的.vimrc下添加:

Plugin 'mk12/vim-lean'

… 然后在Vim中运行以下命令:

:source %
:PluginInstall

对于Vundle版本 < 0.10.2，请用上面的Bundle替换Plugin。

使用NeoBundle管理器安装

在你的.vimrc下添加:

NeoBundle 'mk12/vim-lean'

… 然后在Vim中运行以下命令:

:source %
:NeoBundleInstall

使用VimPlug管理器安装

在你的.vimrc下添加:

Plug 'mk12/vim-lean'

… 然后在Vim中运行以下命令:

:source %
:PlugInstall

使用Pathogen管理器安装

在终端中运行以下命令:

cd ~/.vim/bundle
git clone https://github.com/mk12/vim-lean

Ⅳ. 文档说明

# Vim Lean

This repository is a Pathogen/Vundle/Plug plugin for the Lean Theorem Prover. The files ftdetect/lean.vim and syntax/lean.vim are taken directly from the official lean.vim plugin.

Install

Set up vim-plug, and then add the following to your .vimrc:

Plug 'mk12/vim-lean', { 'for': 'lean' }

Usage

Why use this instead of the official plugin? Because it provides two useful commands:

• :LeanReplace: Replace forall, Pi, ->, etc., with Unicode characters.
• :LeanCheck: Run lean on the file and show the output in a split (if there is any).

Put let g:lean_auto_replace = 1 in your vimrc if you want to run :LeanReplace automatically on every save.

License

The Lean Theorem Prover is available under the Apache License 2.0; see LICENSE for details.