我对以下h定义中证据术语的匹配部分的Coq类型系统的行为感到困惑:
Set Implicit Arguments.
Definition h := fun (a b : nat) (e : a = b) =>
(fun (x y : nat)(HC : b = y)(H : x = y) =>
(match H in (_ = y0) return (b = y0 -> b = x) with
| @eq_refl _ _ => fun HC0 : b = x => HC0
end HC)) a b (eq_refl b) e.
检查h告诉我们整体类型是"forall ab:nat,a = b - > b = a".
由于H的类型是x = y,由于return子句,匹配将返回类型为b = …
参考手册(第14.4节)表明coqchk将获取.vo文件列表并键入检查生成它们的.v文件中的内容.(可能)不太可靠的来源表明.vo文件不包含完整的证明条款.因此问题:.vo文件包含什么？coqchk如何使用该信息执行类型检查？