From a86fae12588d6c540173ab5d7cfcc330e0e00b09 Mon Sep 17 00:00:00 2001
From: Ben Puryear <54869170+Ben10164@users.noreply.github.com>
Date: Thu, 18 Jul 2024 17:50:20 -0700
Subject: [PATCH] Added dpetka's suggestions

---
 lua/lazyvim/plugins/extras/lang/lean.lua | 17 -----------------
 1 file changed, 17 deletions(-)

diff --git a/lua/lazyvim/plugins/extras/lang/lean.lua b/lua/lazyvim/plugins/extras/lang/lean.lua
index 74147e61..890dd8bd 100644
--- a/lua/lazyvim/plugins/extras/lang/lean.lua
+++ b/lua/lazyvim/plugins/extras/lang/lean.lua
@@ -8,9 +8,6 @@ return {
   {
     "Julian/lean.nvim",
     event = { "BufReadPre *.lean", "BufNewFile *.lean" },
-    dependencies = {
-      "nvim-lua/plenary.nvim",
-    },
 
     -- see details below for full configuration options
     opts = {
@@ -22,7 +19,6 @@ return {
       -- In particular ensure you have followed instructions setting up a callback
       -- for `LspAttach` which sets your key bindings!
       lsp = {
-        on_attach = on_attach,
         init_options = {
           -- See Lean.Lsp.InitializationOptions for details and further options.
 
@@ -125,17 +121,4 @@ return {
       },
     },
   },
-  {
-    -- Lean4 has it's own built in lsp
-    -- this is automatically added by lean.nvim
-    "neovim/nvim-lspconfig",
-  },
-  {
-    "hrsh7th/nvim-cmp",
-    optional = true,
-    opts = function(_, opts)
-      opts.sources = opts.sources or {}
-      table.insert(opts.sources, { { name = "nvim_lsp" }, { name = "path" }, { name = "buffer" } })
-    end,
-  },
 }