相关疑难解决方法(0)

在一些依赖类型的语言(例如Idris)中实现向量添加是相当简单的.根据维基百科上的示例:

import Data.Vect

%default total

pairAdd : Num a => Vect n a -> Vect n a -> Vect n a
pairAdd Nil       Nil       = Nil
pairAdd (x :: xs) (y :: ys) = x + y :: pairAdd xs ys

(注意Idris的整体检查器如何自动推断添加Nil和非Nil向量是逻辑上不可能的.)

我正在尝试使用自定义向量实现在Coq中实现等效功能,尽管与官方Coq库中提供的非常相似:

Set Implicit Arguments.

Inductive vector (X : Type) : nat -> Type :=
  | vnul : vector X 0 
  | vcons {n : nat} (h : X) …