2

我从 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 替换为 []）？

如果我尝试在第二种情况下拆分 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，以避免任何干扰。

提前致谢。

注意： 这似乎是 idris 本身的错误？

4

0 回答 0