From a1a918193a05daef7236ccffa8b9e36261f23df5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9ana=20=E6=B1=9F?= <leana.jiang+git@icloud.com>
Date: Sat, 24 Jan 2026 21:22:12 +0100
Subject: [PATCH] nvim/ftplugin: agda support

---
 .config/nvim/ftplugin/agda.vim          | 184 ++++++++++++++++++++++++
 .config/nvim/ftplugin/markdown.agda.vim |   1 +
 .config/nvim/lua/_lazy.lua              |   7 +-
 3 files changed, 191 insertions(+), 1 deletion(-)
 create mode 100644 .config/nvim/ftplugin/agda.vim
 create mode 120000 .config/nvim/ftplugin/markdown.agda.vim

diff --git a/.config/nvim/ftplugin/agda.vim b/.config/nvim/ftplugin/agda.vim
new file mode 100644
index 00000000..74a49940
--- /dev/null
+++ b/.config/nvim/ftplugin/agda.vim
@@ -0,0 +1,184 @@
+" Sourced from
+" https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.VIMEditing#:~:text=agda%2Dutf8%2Evim
+" (Link is dead so use wayback machine)
+
+" Superscripts
+imap <buffer> ^0 ⁰
+imap <buffer> ^1 ¹
+imap <buffer> ^2 ²
+imap <buffer> ^3 ³
+imap <buffer> ^4 ⁴
+imap <buffer> ^5 ⁵
+imap <buffer> ^6 ⁶
+imap <buffer> ^7 ⁷
+imap <buffer> ^8 ⁸
+imap <buffer> ^9 ⁹
+imap <buffer> ^+ ⁺
+imap <buffer> ^- ⁻
+imap <buffer> ^= ⁼
+imap <buffer> ^( ⁽
+imap <buffer> ^) ⁾
+imap <buffer> ^n ⁿ
+
+" Subscripts
+imap <buffer> \_0 ₀
+imap <buffer> \_1 ₁
+imap <buffer> \_2 ₂
+imap <buffer> \_3 ₃
+imap <buffer> \_4 ₄
+imap <buffer> \_5 ₅
+imap <buffer> \_6 ₆
+imap <buffer> \_7 ₇
+imap <buffer> \_8 ₈
+imap <buffer> \_9 ₉
+imap <buffer> \_+ ₊
+imap <buffer> \_- ₋
+imap <buffer> \_= ₌
+imap <buffer> \_( ₍
+imap <buffer> \_) ₎
+
+" Arrows
+imap <buffer> -> →
+imap <buffer> <-- ←
+imap <buffer> <--> ↔
+imap <buffer> ==> ⇒
+imap <buffer> <== ⇐
+imap <buffer> <==> ⇔
+"
+" Symbols from mathematics and logic, LaTeX style
+imap <buffer> \forall ∀
+imap <buffer> \exists ∃
+imap <buffer> \in ∈
+imap <buffer> \ni ∋
+imap <buffer> \empty ∅
+imap <buffer> \prod ∏
+imap <buffer> \sum ∑
+imap <buffer> \le ≤
+imap <buffer> \ge ≥
+imap <buffer> \pm ±
+imap <buffer> \subset ⊂
+imap <buffer> \subseteq ⊆
+imap <buffer> \supset ⊃
+imap <buffer> \supseteq ⊇
+imap <buffer> \setminus ∖
+imap <buffer> \cap ∩
+imap <buffer> \cup ∪
+imap <buffer> \int ∫
+imap <buffer> \therefore ∴
+imap <buffer> \qed ∎
+imap <buffer> \1 𝟙
+imap <buffer> \N ℕ
+imap <buffer> \Z ℤ
+imap <buffer> \C ℂ
+imap <buffer> \Q ℚ
+imap <buffer> \R ℝ
+imap <buffer> \E 𝔼
+imap <buffer> \F 𝔽
+imap <buffer> \to →
+imap <buffer> \mapsto ↦
+imap <buffer> \infty ∞
+imap <buffer> \equiv ≡
+imap <buffer> \cong ≅
+imap <buffer> \:= ≔
+imap <buffer> \=: ≕
+imap <buffer> \ne ≠
+imap <buffer> \approx ≈
+imap <buffer> \perp ⊥
+imap <buffer> \not ̷
+imap <buffer> \ldots …
+imap <buffer> \cdots ⋯
+imap <buffer> \cdot ⋅
+imap <buffer> \circ ◦
+imap <buffer> \times ×
+imap <buffer> \oplus ⊕
+imap <buffer> \langle ⟨
+imap <buffer> \rangle ⟩
+
+" Math
+imap <buffer> \monus ∸
+
+" Greek alphabet...
+imap <buffer> \alpha α
+imap <buffer> \beta β
+imap <buffer> \gamma γ
+imap <buffer> \delta δ
+imap <buffer> \epsilon ε
+imap <buffer> \zeta ζ
+imap <buffer> \nu η
+imap <buffer> \theta θ
+imap <buffer> \iota ι
+imap <buffer> \kappa κ
+imap <buffer> \lambda λ
+imap <buffer> \mu μ
+imap <buffer> \nu ν
+imap <buffer> \xi ξ
+imap <buffer> \omicron ο
+imap <buffer> \pi π
+imap <buffer> \rho ρ
+imap <buffer> \stigma ς
+imap <buffer> \sigma σ
+imap <buffer> \tau τ
+imap <buffer> \upsilon υ
+imap <buffer> \phi ϕ
+imap <buffer> \varphi φ
+imap <buffer> \chi χ
+imap <buffer> \psi ψ
+imap <buffer> \omega ω
+
+imap <buffer> \Alpha Α
+imap <buffer> \Beta Β
+imap <buffer> \Gamma Γ
+imap <buffer> \Delta Δ
+imap <buffer> \Epsilon Ε
+imap <buffer> \Zeta Ζ
+imap <buffer> \Nu Η
+imap <buffer> \Theta Θ
+imap <buffer> \Iota Ι
+imap <buffer> \Kappa Κ
+imap <buffer> \Lambda Λ
+imap <buffer> \Mu Μ
+imap <buffer> \Nu Ν
+imap <buffer> \Xi Ξ
+imap <buffer> \Omicron Ο
+imap <buffer> \Pi Π
+imap <buffer> \Rho Ρ
+imap <buffer> \Sigma Σ
+imap <buffer> \Tau Τ
+imap <buffer> \Upsilon Υ
+imap <buffer> \Phi Φ
+imap <buffer> \Chi Χ
+imap <buffer> \Psi Ψ
+imap <buffer> \Omega Ω
+
+" autoload
+function! CornelisLoadWrapper()
+  if exists(":CornelisLoad") ==# 2
+    CornelisLoad
+  endif
+endfunction
+
+au BufReadPre *.agda call CornelisLoadWrapper()
+au BufReadPre *.lagda* call CornelisLoadWrapper()
+
+au BufRead,BufNewFile *.agda call AgdaFiletype()
+au BufRead,BufNewFile *.lagda* call AgdaFiletype()
+au QuitPre *.agda :CornelisCloseInfoWindows
+au QuitPre *.lagda* :CornelisCloseInfoWindows
+
+" autoreload at file write
+au BufWritePost *.agda execute "normal! :CornelisLoad\<CR>"
+au BufWritePost *.lagda* execute "normal! :CornelisLoad\<CR>"
+
+" default cornelis config
+nnoremap <buffer> <leader>l :CornelisLoad<CR>
+nnoremap <buffer> <leader>r :CornelisRefine<CR>
+nnoremap <buffer> <leader>d :CornelisMakeCase<CR>
+nnoremap <buffer> <leader>, :CornelisTypeContext<CR>
+nnoremap <buffer> <leader>. :CornelisTypeContextInfer<CR>
+nnoremap <buffer> <leader>n :CornelisSolve<CR>
+nnoremap <buffer> <leader>a :CornelisAuto<CR>
+nnoremap <buffer> gd        :CornelisGoToDefinition<CR>
+nnoremap <buffer> [/        :CornelisPrevGoal<CR>
+nnoremap <buffer> ]/        :CornelisNextGoal<CR>
+nnoremap <buffer> <C-A>     :CornelisInc<CR>
+nnoremap <buffer> <C-X>     :CornelisDec<CR>
diff --git a/.config/nvim/ftplugin/markdown.agda.vim b/.config/nvim/ftplugin/markdown.agda.vim
new file mode 120000
index 00000000..72fd5ccf
--- /dev/null
+++ b/.config/nvim/ftplugin/markdown.agda.vim
@@ -0,0 +1 @@
+.config/nvim/ftplugin/agda.vim
\ No newline at end of file
diff --git a/.config/nvim/lua/_lazy.lua b/.config/nvim/lua/_lazy.lua
index 8784d253..c388d328 100644
--- a/.config/nvim/lua/_lazy.lua
+++ b/.config/nvim/lua/_lazy.lua
@@ -124,7 +124,12 @@ local plugins = {
         "agda/cornelis",
         name = "cornelis",
         ft = "agda",
-        init = function() vim.g.cornelis_use_global_binary = 1 end,
+        init = function()
+            vim.g.cornelis_use_global_binary = 1
+            -- We don't use the default binding for shortcuts (see ftplugin)
+            -- Also, buffer reload is done in the ftplugin too
+            vim.g.cornelis_no_agda_input = 1
+        end,
         dependencies = { "neovimhaskell/nvim-hs.vim", "kana/vim-textobj-user" },
         version = "*",
     },