如何比较Agda中Nats的矢量图

Question

我正在尝试使用Decidable Equality来比较Agda中的两个Nats向量.我尝试打开Vector Equality模块,将Nat DecSetoid作为参数传递,如下所示:

open import Data.Nat
open import Data.Vec

open import Relation.Binary.PropositionalEquality
import Data.Vec.Equality

myFunction : {n : ?} -> Vec ? n -> Vec ? n -> ? 
myFunction v1 v2 
  with v1 Data.Vec.Equality.DecidableEquality.? v2
... | _  =  {!!}
  where 
    open Data.Vec.Equality.DecidableEquality  (Relation.Binary.PropositionalEquality.decSetoid Data.Nat._?_) 

但是,我收到以下错误:

Vec ? .n !=< .Relation.Binary.DecSetoid (_d?_6 v1 v2) (_d?_7 v1 v2)
of type Set
when checking that the expression v1 has type
.Relation.Binary.DecSetoid (_d?_6 v1 v2) (_d?_7 v1 v2)

我不确定我做错了什么.我使用的模块系统是错误的,还是我需要以不同的方式使用？？

Answer 1

这里的问题是该where子句没有将标识符放在表达式的范围内with.因此,当你使用时Data.Vec.Equality.DecidableEquality.?,你并没有引用专门用于自然数向量的那个,而是用于定义的一般向量Data.Vec.Equality.这就是为什么Agda期望DecSetoid作为第一个论点并抱怨.

可能的解决方法是先命名您感兴趣的模块,然后使用限定名称来引用它_?_.通过以下方式定义别名,我冒昧地使用较短的名称as:

open import Relation.Binary.PropositionalEquality as PropEq
import Data.Vec.Equality as VecEq

module VecNatEq = VecEq.DecidableEquality (PropEq.decSetoid Data.Nat._?_)

myFunction : {n : ?} -> Vec ? n -> Vec ? n -> ? 
myFunction v1 v2 
  with v1 VecNatEq.? v2
... | _  =  {!!}