From f088d05a14c794be0b1168103c1f8f6ec54b4a5a Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Tue, 28 Dec 2021 09:56:16 +0100
Subject: [PATCH] add \T to show type with implicits

---
 ftplugin/idris2.vim | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/ftplugin/idris2.vim b/ftplugin/idris2.vim
index 4ef20e5..cbb3726 100644
--- a/ftplugin/idris2.vim
+++ b/ftplugin/idris2.vim
@@ -118,13 +118,13 @@ function! IdrisReloadToLine(cline)
   "return tc
 endfunction
 
-function! IdrisShowType()
+function! IdrisShowType(imp)
   w
   let word = s:currentQueryObject()
   let cline = line(".")
   let ccol = col(".")
-    let ty = s:IdrisCommand(":t", word)
-    call IWrite(ty)
+  let ty = s:IdrisCommand(a:imp ? ":ti" : ":t", word)
+  call IWrite(ty)
 endfunction
 
 function! IdrisShowDoc()
@@ -295,7 +295,8 @@ function! IdrisEval()
   call IWrite(" = " . result)
 endfunction
 
-nnoremap <buffer> <silent> <LocalLeader>t :call IdrisShowType()<ENTER>
+nnoremap <buffer> <silent> <LocalLeader>t :call IdrisShowType(0)<ENTER>
+nnoremap <buffer> <silent> <LocalLeader>T :call IdrisShowType(1)<ENTER>
 nnoremap <buffer> <silent> <LocalLeader>r :call IdrisReload(0)<ENTER>
 nnoremap <buffer> <silent> <LocalLeader>c :call IdrisCaseSplit()<ENTER>
 nnoremap <buffer> <silent> <LocalLeader>a 0:call search(":")<ENTER>b:call IdrisAddClause(0)<ENTER>w