如何解决Agda stdlib Vec from任意长度的列表列表
我正在尝试在任意长度的Data.Vec
上使用fromList
Data.List
:
natListToVec : {n : ℕ} → List ℕ → Vec ℕ n
natListToVec nats = v.fromList nats
但是得到错误:
l.foldr (λ _ → suc) 0 nats != n of type ℕ
when checking that the expression fromList nats has type Vec ℕ n
当我尝试使用长度已知的List
时,我不会遇到任何问题:
ListWith2ToVec : v.fromList (2 l.∷ l.[]) ≡ 2 v.∷ v.[]
ListWith2ToVec = refl
我猜问题在于这种类型签名:
{n : ℕ} → List ℕ → Vec ℕ n
我没有指定n必须为List ℕ
的长度。
我该怎么做?
谢谢!
解决方法
您可以简单地在类型签名中使用length
函数。您还必须命名类型为list的参数来引用它,就像这样:
natListToVec : (xs : List ℕ) → Vec ℕ (length xs)
[...]
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。