小编adH*_*ush的帖子

我对idris和依赖类型相对较新,我遇到了以下问题 - 我创建了一个类似于矢量的自定义数据类型:

infixr 1 :::

data TupleVect : Nat -> Nat -> Type -> Type where
    Empty : TupleVect Z Z a
    (:::) : (Vect o a, Vect p a) ->
            TupleVect n m a ->
            TupleVect (n+o) (m+p) a

exampleTupleVect : TupleVect 5 4 Int
exampleTupleVect = ([1,2], [1]) ::: ([3,4],[2,3]) ::: ([5], [4]) ::: Empty

它通过添加向量元组并通过每个元组位置中的向量长度之和进行索引来归纳构造.

我试图为我的数据类型实现一个map函数:

tupleVectMap : ((Vect k a, Vect l a) -> (Vect k b, Vect l b)) ->
               TupleVect n m a …