私はidrisとidris-vimから始めています。しかし\c (IdrisCaseSplit)、私がいる行を削除することがあります。私は次のプログラムで試します：
vApp : Vect n (a -> b) -> Vect n a -> Vect n b
次に、カーソルを上に置いてvApp押す\dと、次のようになります。
vApp : Vect n (a -> b) -> Vect n a -> Vect n b
vApp xs ys = ?vApp_rhs
最初のケースに移動しxsて押す\cと、次のようになります。
vApp : Vect n (a -> b) -> Vect n a -> Vect n b
vApp [] ys = ?vApp_rhs_1
vApp (x :: xs) ys = ?vApp_rhs_2
ここまでは順調ですがys、最初のケース ( vApp [] ys) に移動して を押す\cと、行全体が削除されます。
なぜ行が削除されたのですか？望ましい動作を得るにはどうすればよいですか (ys を [] に置き換えます)。
2 番目のケースで ys をケース分割しようとすると、同じことが起こりvApp (x :: xs) ysます。
- Mac OSX、VIM 7.4 で idris 0.9.14.3 を使用しています。
- 病原体で活性化されたidris-vim。
- idris-vim は動作しています (たとえば、\t は正常に動作します)。
- :map
\cは、実際にマップされているものを返します:call IdrisCaseSplit()<CR> - 干渉を避けるために、最小限のvimrcで試しました。
前もって感謝します。