小编Nic*_*ann的帖子

我用opam安装了Coq，并想制作一个Coq插件。我设法使用编译了一些插件示例coq_makefile，但是如果我可以在vim中使用merlin来获取类型信息并完成Coq库，那将是很棒的。

有没有一种方法可以将Coq库添加到ocamlfind？

我试图get使用子集类型为列表执行安全功能.我用程序试了这个定义

Program Fixpoint get A (l : list A) (n : {x : nat | x < length l} ) : A :=
  match (n, l) with
  | (O, x :: l') => x
  | (S n', x :: l') => get l' n'
  | _ => _
  end.

问题是它得到以下错误

Found a constructor of inductive type nat while a constructor of sig is expected.

为什么coq不允许我在包含子集类型的对中进行模式匹配？