From 82226b4f78de14694a0acd4d76a15c3af4d13beb Mon Sep 17 00:00:00 2001 From: yannickreiss Date: Tue, 8 Jul 2025 19:59:46 +0200 Subject: [PATCH] Add lean snippets and do Neovide --- UltiSnips/lean.snippets | 26 ++++++++++++++++++++++++++ lua/plugins.lua | 26 ++++++++++++++++++++++++++ lua/vanilla.lua | 1 - 3 files changed, 52 insertions(+), 1 deletion(-) create mode 100644 UltiSnips/lean.snippets diff --git a/UltiSnips/lean.snippets b/UltiSnips/lean.snippets new file mode 100644 index 0000000..8c79516 --- /dev/null +++ b/UltiSnips/lean.snippets @@ -0,0 +1,26 @@ +snippet ß "Backslash" A +\\ +endsnippet + +snippet <> "Add sharp brackets" +⟨$1⟩$0 +endsnippet + +# Mengen +snippet N "Natural number" +ℕ +endsnippet + +snippet Z "Whole numbers" +ℤ +endsnippet + + +# Quantoren +snippet E "Exists" +∃ +endsnippet + +snippet A "All" +∀ +endsnippet diff --git a/lua/plugins.lua b/lua/plugins.lua index 160280b..cfc7685 100644 --- a/lua/plugins.lua +++ b/lua/plugins.lua @@ -111,4 +111,30 @@ return { { "wT", "lua require('neowiki').open_wiki_new_tab()", desc = "Open Wiki in Tab" }, }, }, + + -- Lean + { + "Julian/lean.nvim", + event = { "BufReadPre *.lean", "BufNewFile *.lean" }, + + dependencies = { + "neovim/nvim-lspconfig", + "nvim-lua/plenary.nvim", + + -- optional dependencies: + + -- a completion engine + -- hrsh7th/nvim-cmp or Saghen/blink.cmp are popular choices + + -- 'nvim-telescope/telescope.nvim', -- for 2 Lean-specific pickers + -- 'andymass/vim-matchup', -- for enhanced % motion behavior + -- 'andrewradev/switch.vim', -- for switch support + -- 'tomtom/tcomment_vim', -- for commenting + }, + + ---@type lean.Config + opts = { -- see below for full configuration options + mappings = true, + }, + }, } diff --git a/lua/vanilla.lua b/lua/vanilla.lua index 6029ac4..fb2823e 100644 --- a/lua/vanilla.lua +++ b/lua/vanilla.lua @@ -29,7 +29,6 @@ vim.opt.encoding = "UTF-8" vim.g.tex_flavor = "latex" vim.opt.conceallevel = 2 vim.opt.showmatch = true -vim.o.guifont = "Source Code Pro:h13" -- set color scheme vim.opt.termguicolors = true