RIP Lean 3.

Julian · Nov 24, 2024 · af6d896 · af6d896
1 parent 1fd2194
commit af6d896
Showing 1 changed file with 6 additions and 8 deletions.
diff --git a/.config/nvim/after/ftplugin/lean.lua b/.config/nvim/after/ftplugin/lean.lua
@@ -4,14 +4,12 @@ vim.wo.signcolumn = 'yes'
 vim.bo.textwidth = 100
 
 vim.keymap.set('n', '<LocalLeader>g', function()
-    require'telescope.builtin'.live_grep{
-      glob_pattern = '*.lean',
-      path_display = { 'tail' },
-      search_dirs = require('lean').current_search_paths()
-    }
+  require'telescope.builtin'.live_grep{
+    glob_pattern = '*.lean',
+    path_display = { 'tail' },
+    search_dirs = require('lean').current_search_paths()
+  }
 end, { buffer = true, desc = 'live grep the Lean search path.' })
 vim.keymap.set('n', '<LocalLeader>l', function()
-    require'telescope'.extensions.loogle.loogle{}
+  require'telescope'.extensions.loogle.loogle{}
 end, { buffer = true, desc = 'search Loogle via Telescope' })
-
-vim.cmd.highlight('link leanTactic Green')