patrick/nix-dotfiles
1
0
Fork 0
mirror of https://github.com/Smaug123/nix-dotfiles synced 2025-10-10 08:58:39 +00:00
Code Issues Packages Projects Releases Wiki Activity

Update flake (breaks ;; in which-key) (#67)

Browse Source
This commit is contained in:
Patrick Stevens
2024-08-06 20:14:01 +01:00
committed by GitHub
parent 19e8024a13
commit ede76d2bc2
12 changed files with 181 additions and 240 deletions
Download Patch File Download Diff File Expand all files Collapse all files

24
home-manager/nvim/lean.lua
View File

@@ -2,16 +2,16 @@ require("lspconfig")["leanls"].setup({})
require("lean").setup({})
require("which-key").register({
l = {
i = { "<Cmd>LeanInfoviewToggle<CR>", "Toggle Lean info view" },
p = { "<Cmd>LeanInfoviewPinTogglePause<CR>", "Pause Lean info view" },
s = { "<Cmd>LeanSorryFill<CR>", "Fill open goals with sorry" },
w = { "<Cmd>LeanInfoviewEnableWidgets<CR>", "Enable Lean widgets" },
W = { "<Cmd>LeanInfoviewDisableWidgets<CR>", "Disable Lean widgets" },
["?"] = {
"<Cmd>LeanAbbreviationsReverseLookup<CR>",
"Show what Lean abbreviation produces the symbol under the cursor",
},
require("which-key").add({
{ "<localleader>l", desc = "Lean" },
{ "<localleader>li", "<Cmd>LeanInfoviewToggle<CR>", desc = "Toggle Lean info view" },
{ "<localleader>lp", "<Cmd>LeanInfoviewPinTogglePause<CR>", desc = "Pause Lean info view" },
{ "<localleader>ls", "<Cmd>LeanSorryFill<CR>", desc = "Fill open goals with sorry" },
{ "<localleader>lw", "<Cmd>LeanInfoviewEnableWidgets<CR>", desc = "Enable Lean widgets" },
{ "<localleader>lW", "<Cmd>LeanInfoviewDisableWidgets<CR>", desc = "Disable Lean widgets" },
{
"<localleader>l?",
"<Cmd>LeanAbbreviationsReverseLookup<CR>",
desc = "Show what Lean abbreviation produces the symbol under the cursor",
},
}, { prefix = vim.api.nvim_get_var("maplocalleader") })
})