idris2-vim icon indicating copy to clipboard operation
idris2-vim copied to clipboard
verified publisher icon edwinb

Fix mapping for adding initial clause

Open vmarkushin opened this issue 5 years ago • 1 comments

vmarkushin avatar Jun 06 '20 18:06 vmarkushin

Sorry to be so slow at noticing this, I'm not keeping up with this repo. a is expected, though - b used to work for adding the body of an interface but that isn't yet implemented in Idris 2. Probably both should be the same key anyway.

edwinb avatar Nov 26 '20 15:11 edwinb