From fafa8c9793d378a568f40427f0c915084c7f48b7 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 7 Dec 2021 14:30:02 +0100 Subject: [PATCH] New lean.nvim features. --- vimrc | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/vimrc b/vimrc index e834df7..dc2ae85 100644 --- a/vimrc +++ b/vimrc @@ -203,10 +203,10 @@ lua <lua vim.lsp.diagnostic.goto_next() nnoremap q lua vim.lsp.diagnostic.set_loclist() nnoremap f lua vim.lsp.buf.formatting() -nnoremap i lua require('lean.infoview').toggle() +" nnoremap i lua require('lean.infoview').toggle() +au filetype lean,lean3 nnoremap K LeanLineDiagnostics nnoremap Telescope find_files nnoremap ff Telescope find_files