vim: add commands for (term)goals

This commit is contained in:
Gabriel Ebner 2021-12-12 12:08:01 +01:00
parent fc8a90331a
commit 8f654a5cbf

2
vimrc

@ -372,6 +372,8 @@ nnoremap <space>f <cmd>lua vim.lsp.buf.formatting()<CR>
" nnoremap <leader>i <Cmd>lua require('lean.infoview').toggle()<CR>
au filetype lean,lean3 nnoremap <buffer> <leader>K <CMD>LeanLineDiagnostics<CR>
au filetype lean,lean3 nnoremap <buffer> <leader>g <CMD>LeanGoal<CR>
au filetype lean nnoremap <buffer> <leader>G <CMD>LeanTermGoal<CR>
nnoremap <c-p> <cmd>Telescope find_files<cr>
nnoremap <leader>ff <cmd>Telescope find_files<cr>